engine · coq · Tangled

forked from coq/coq

coq engine

41 files

coqbot-app[bot] · Merge PR #22631: Export the locations of universes and the universe subgraph · 2w ago

Remove compat coq-core libraries (not executables)

Remove compare_head_gen_with from the Constr API.

Slight cleanup in eq_constr_univs_test

Allow record syntax for record with anonymous fields

Allow record syntax for record with anonymous fields

Remove unnecessary removed_evars membership checks

Take a qualid in Evarnames.resolve.

Remove compare_head_gen_with from the Constr API.

Remove the name field from projections.

More informative printing of template universes

More informative printing of template universes

rewrite logic_monad split in terms of run and reflect

logic_monad.mli

Simplify list_view / reified types in logic_monad

Use the now correct set and maps Names APIs.

Remove the dead Namegen.head_name function.

Nameops.root_of_id don't fail on invalid idents

Add API Nameops.Fresh.union

Introduce PolyFlags to gather flags for polymorphic defs

Introduce PolyFlags to gather flags for polymorphic defs

profile_tactic.ml

Abstract away the Summary reference type.

profile_tactic.mli

Move ltac profiling cutoff away from global flags

proofview_monad.ml

Introduce PolyFlags to gather flags for polymorphic defs

proofview_monad.mli

Introduce PolyFlags to gather flags for polymorphic defs

tclCASE use result instead of adhoc type

tclCASE use result instead of adhoc type

Remove the name field from projections.

Remove the name field from projections.

More precise type for UnivFlex.constrain_variables.

More precise type for UnivFlex.constrain_variables.

changed |= to | when displaying universes constraints

Avoid conflict between global sorts defined in separate modules

More precise type for UnivMinim.normalize_context_set.

More precise type for UnivMinim.normalize_context_set.

QGlobal is not QVar

QGlobal is not QVar

QLeq has nothing to do with elimination

univProblem.mli

feat: Add elim constraint elaboration

Lift big closures to reduce memory consumption

Remove the QCumulConstraint type for good.

Merge PR #22631: Export the locations of universes and the universe subgraph

Merge PR #22631: Export the locations of universes and the universe subgraph