1
2
3
4
5
6
7
8
9
10
11
12
13
|
pred log.coq.env.add-section-variable-noimplicits i:id, i:term, o:constant.
log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [
if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
% elpi:if version coq-elpi < 2.4.0
@local! => coq.env.add-section-variable ID Ty C,
% elpi:endif
% elpi:if version coq-elpi >= 2.4.0
@local! => coq.env.add-section-variable ID _ Ty C,
% elpi:endif
log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
@local! => log.coq.arguments.set-implicit (const C) [[]],
].
|
