proofs · coq · Tangled

forked from coq/coq

coq proofs

20 files

Pierre-Marie Pédrot · Extrude universe abstraction of general definitions out of the kernel. · 1mo ago

Fix has_dependent_elim to handle postponed eta

Print evars instead of metas in Clenv unification failures

Remove compat coq-core libraries (not executables)

Take a qualid in Evarnames.resolve.

goal_select.mli

Remove SelectNth and SelectId

Abstract the val variant of context datatypes.

Keep track of variable status (secvar or not) in named contexts

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

proof_bullet.ml

Rename Coq -> Rocq in various comments and doc

proof_bullet.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Restore "Proof Using Clear Unused"

Restore "Proof Using Clear Unused"

Keep track of variable status (secvar or not) in named contexts

Update the OCaml headers to reflect the fact Coq is now Rocq.

Extrude universe abstraction of general definitions out of the kernel.

Stop inlining abstracted subproofs in tactics in terms.

Keep track of variable status (secvar or not) in named contexts

Deprecate Tacmach.pf_apply.

document tactics/tactics.mli