We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 255e7e4 commit 57b2cb7Copy full SHA for 57b2cb7
apps/derive/elpi/eqType.elpi
@@ -86,7 +86,7 @@ irrelevant? (app [{{ @eq }}, global EqType, A, B]) (eqb.app EQ EQTYPE [A1,B1]) D
86
term->trm A A1,
87
term->trm B B1,
88
].
89
-irrelevant? T R D :- whd1 T T1, coq.say "whd" T T1, irrelevant? T1 R D.
+irrelevant? T R D :- whd1 T T1, irrelevant? T1 R D.
90
91
pred term->trm i:term, o:eqb.trm, o:diagnostic.
92
term->trm (global GR) (eqb.global GR) ok :- !.
0 commit comments