From f79d8f27e6f7e6bacee02d2b5f996a3b2b87cd98 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 14 Nov 2024 14:03:59 +0100 Subject: [PATCH] wip --- apps/derive/elpi/eqbcorrect.elpi | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi index f6ae3919b..388ccbe7b 100644 --- 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". %---------------------------------------------------------------------------