wip

LPCIC · Nov 14, 2024 · 86a27c4 · 86a27c4
1 parent 1cd391b
commit 86a27c4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/apps/derive/elpi/eqbOK.elpi b/apps/derive/elpi/eqbOK.elpi
@@ -60,6 +60,6 @@ main (const C) Prefix [CL] :- std.do! [
   CL = eqbok-for (const C) Reflect,
   coq.elpi.accumulate _ "derive.eqbOK.db" (clause _ _ CL),
 ].
-main (indc _) _ _ :- /*stop*/ coq.error "cannot call eqbOK on a constructor".
+main (indc _) _ _ :- stop "cannot call eqbOK on a constructor".
 
 }
diff --git a/apps/derive/theories/derive/eqbOK.v b/apps/derive/theories/derive/eqbOK.v
@@ -14,6 +14,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive
 Elpi Db derive.eqbOK.db lp:{{
 
   pred eqbok-for o:gref, o:constant.
+  type stop string -> prop.
 
 }}.
-Original file line number
+Diff line change
@@ Expand Up @@
     Elpi Db derive.eqbOK.db lp:{{
       pred eqbok-for o:gref, o:constant.
+      type stop string -> prop.
     }}.
@@ Expand Down @@