File: compat_add_secvar_18_19.elpi

package info (click to toggle)
coq-hierarchy-builder 1.8.1-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,988 kB
  • sloc: makefile: 109
file content (8 lines) | stat: -rw-r--r-- 408 bytes parent folder | download 
1
2
3
4
5
6
7
8
 
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),
  @local! => coq.env.add-section-variable ID Ty C,
  log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
  @local! => log.coq.arguments.set-implicit (const C) [[]],
].