Skip to content

Commit 4ce351c

Browse files
gareseponier
andcommitted
Update apps/derive/elpi/eqbcorrect.elpi
Co-authored-by: Jean-Christophe Léchenet <[email protected]>
1 parent d5cdcf6 commit 4ce351c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

apps/derive/elpi/eqbcorrect.elpi

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -413,7 +413,7 @@ search What Rec (app [GR|L] as GRL) R :- !, std.do! [
413413
search What _Rec (global GR as GRL) {{ fun (x : lp:GRL) (_ : lp:IsGR x) => lp:R x }} :-
414414
What (global GR) R,
415415
mk-reali (global GR) IsGR, !.
416-
search What _ X _ :- coq.safe-dest-app X HD _, std.assert! (What HD _) "run eqbcorrect before.".
416+
search What _ X _ :- coq.safe-dest-app X HD _, std.assert! (What HD _) "run eqbcorrect before".
417417

418418
pred apply-aux i:term, i:list term, o:term.
419419
apply-aux Aux [] Aux.

0 commit comments

Comments
 (0)