wip

LPCIC · Nov 14, 2024 · f79d8f2 · f79d8f2
1 parent 86a27c4
commit f79d8f2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi
@@ -3,7 +3,7 @@
 /* ------------------------------------------------------------------------- */
 
 type feqb.trm->term trm -> term -> prop.
-% type stop string -> prop.
+type stop string -> prop.
 
 macro @pi-trm N T F :-
   pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.
@@ -97,7 +97,7 @@ main (const C) Prefix [Clause] :- std.do! [
   Clause = (eqcorrect-for (const C) CC CR),
   coq.elpi.accumulate _ "derive.eqbcorrect.db" (clause _ _ Clause),
 ].
-main (indc _) _ _ :- /*stop*/ coq.error "derive.eqbcorrect does not work on a constructor".
+main (indc _) _ _ :- stop "derive.eqbcorrect does not work on a constructor".
 
 %---------------------------------------------------------------------------