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 4f8edb4 commit bc70317Copy full SHA for bc70317
HB/common/log.elpi
@@ -71,7 +71,12 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
71
pred env.add-section-variable-noimplicits i:id, i:term, o:constant.
72
env.add-section-variable-noimplicits Name Ty C :- std.do! [
73
if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
74
+% elpi:if version coq-elpi < 2.4.0
75
+ @local! => coq.env.add-section-variable ID Ty C,
76
+% elpi:endif
77
+% elpi:if version coq-elpi >= 2.4.0
78
@local! => coq.env.add-section-variable ID _ Ty C,
79
80
log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
81
@local! => arguments.set-implicit (const C) [[]],
82
].
0 commit comments