Apply suggestions from code review

math-comp · Dec 12, 2024 · 9d592ee · 9d592ee
1 parent 521adf9
commit 9d592ee
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
@@ -243,7 +243,7 @@ instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
   factory-alias->gref TmGR M,
   std.mem! ML M,
   !,
-  if (mixin-for T M X) true (coq.error "Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !,
+  if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !,
   instantiate-all-these-mixin-args (F X) T ML R.
 instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !,
   @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m).

diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out
@@ -1,2 +1,2 @@
 The command has indeed failed with message:
-Unable to find mixin err_miss_dep_IsAddComoid on subject K
+HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K