plugins/firstorder · coq · Tangled

forked from coq/coq

coq plugins firstorder

15 files

coqbot-app[bot] · Merge PR #22074: Remove more global lazys · 5mo ago

Remove compat coq-core libraries (not executables)

Move the dubious compare and hash functions from Constr to a Termops submodule.

Stop relying on atoms to discriminate goal formulas in firstorder.

Remove more global lazys

Rename the Pcoq module into Procq.

Deprecate Tacmach.pf_env.

Clean up the Firstorder implementation.

Move the dubious compare and hash functions from Constr to a Termops submodule.

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

Stop opening Tacmach module and qualify uses instead.

Do not store the domain pattern in left-hand-side firstorder arrow pattern.

Stop relying on atoms to discriminate goal formulas in firstorder.

Stop keeping track of hypotheses in a dedicated firstorder context.

Move the dubious compare and hash functions from Constr to a Termops submodule.

Use a fast path in Unify.unify_atom.