Merge pull request #478 from math-comp/fix-error-mising-dep

improve error message missing mixin dep

Author: CohenCyril

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,
   !,
-  mixin-for T M X, !,
+  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).

Makefile.test-suite.coq.local

@@ -23,4 +23,5 @@ post-all::
 	$(call DIFF, tests/howto.v)
 	$(call DIFF, tests/missing_join_error.v)
 	$(call DIFF, tests/not_same_key.v)
-	$(call DIFF, tests/hnf.v)
+	$(call DIFF, tests/hnf.v)
+	$(call DIFF, tests/err_miss_dep.v)

tests/err_miss_dep.v

@@ -0,0 +1,6 @@
+From HB Require Import structures.
+HB.mixin Record IsAddComoid A := {}.
+HB.structure Definition AddComoid := { A of IsAddComoid A }.
+HB.mixin Record IsAbelianGrp A of IsAddComoid A := {}.
+HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }.
+Fail HB.mixin Record IsRing K of IsAbelianGrp K (*& IsAddComoid K*) := {}.

tests/err_miss_dep.v.out

@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K