plugins/funind · coq · Tangled

forked from coq/coq

coq plugins funind

21 files

Pierre-Marie Pédrot · Use the now correct set and maps Names APIs. · 1mo ago

Remove compat coq-core libraries (not executables)

functional_principles_proofs.ml

Rename is_section_variable' -> is_section_variable_env

functional_principles_proofs.mli

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

functional_principles_types.ml

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

functional_principles_types.mli

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

QGlobal is not QVar

Use of QualityOrSet in elimination scheme generation

gen_principle.ml

Implement `{| foo with fields |}` for terms

gen_principle.mli

Use of QualityOrSet in elimination scheme generation

glob_term_to_relation.ml

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

glob_term_to_relation.mli

[ocamlformat] Enable for funind.

glob_termops.ml

Use variable status to decide if a variable is section variable

glob_termops.mli

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

indfun_common.ml

Use the now correct set and maps Names APIs.

indfun_common.mli

Stop using global lazy in funind

Reduce the exposure of QualityOrSet.t type in the Retyping API.

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

Remove the not extremely well-named Inv.inv function.

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

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

[declare] Move proof information to declare.