Merge pull request #479 from math-comp/fix-error-missing-key

specific error for missing subject

Author: CohenCyril

HB/instance.elpi

@@ -57,13 +57,17 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
     UnfoldClauses => copy SectionTy SectionTyUnfolded,
   ]) (SectionTy = SectionTyUnfolded),
 
+  % call HB.instance TheType TheFactory
+  std.drop NParams Args [TheType|_],
+
+  if (var TheType)
+    (coq.error "HB: The instance subject must be explicitly given.\nUse:\n  HB.instance Definition _ : M <subject> := ...\n  HB.instance Definition _ := M.Build <subject> ...")
+    true,
+
   log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
     SectionTyUnfolded @transparent! C,
   TheFactory = (global (const C)),
 
-  % call HB.instance TheType TheFactory
-  std.drop NParams Args [TheType|_],
-
   private.check-non-forgetful-inheritance TheType Factory,
 
   private.declare-instance Factory TheType TheFactory Clauses CSL,

Makefile.test-suite.coq.local

@@ -18,6 +18,7 @@ DIFF=\
 	fi
 
 post-all::
+	$(call DIFF, tests/err_missin_subject.v)
 	$(call DIFF, tests/compress_coe.v)
 	$(call DIFF, tests/about.v)
 	$(call DIFF, tests/howto.v)

tests/err_missin_subject.v

@@ -0,0 +1,6 @@
+From HB Require Import structures.
+HB.mixin Record M X := {}.
+HB.structure Definition S := { X of M X}.
+HB.instance Definition _ : M nat := M.Build _.
+HB.instance Definition _ : M _ := M.Build bool.
+Fail HB.instance Definition _ : M _ := M.Build _.

tests/err_missin_subject.v.out

@@ -0,0 +1,5 @@
+The command has indeed failed with message:
+HB: The instance subject must be explicitly given.
+Use:
+  HB.instance Definition _ : M <subject> := ...
+  HB.instance Definition _ := M.Build <subject> ...