coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/constr.ml

September 2026

coqbot-app[bot]
Merge PR #22526: Reduce the equality APIs in Constr
committed
Pierre-Marie Pédrot
Remove compare_head_gen_with from the Constr API.
committed
Pierre-Marie Pédrot
Remove Constr.eq_constr_nounivs.
committed
Pierre-Marie Pédrot
Reduce the equality APIs in Constr.
committed

June 2026

coqbot-app[bot]
Merge PR #21987: Keep track of which variables are section variables and use this info to fix bugs
committed

May 2026

Gaëtan Gilbert
Move CompactedDecl to ppconstr
committed

April 2026

coqbot-app[bot]
Merge PR #21863: Move the dubious compare and hash functions from Constr to a Termops submodule
committed
Pierre-Marie Pédrot
Move the dubious compare and hash functions from Constr to a Termops submodule.
committed

March 2026

coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed
coqbot-app[bot]
Merge PR #21712: Inline Sorts.is_small in its only caller
committed
Gaëtan Gilbert
Inline Sorts.is_small in its only caller
committed

February 2026

coqbot-app[bot]
Merge PR #21646: case styles MatchStyle and RegularStyle are the same
committed
Gaëtan Gilbert
case styles MatchStyle and RegularStyle are the same
committed

January 2026

coqbot-app[bot]
Merge PR #21508: Stop unifying sorts in the kernel.
committed
Pierre-Marie Pédrot
Simplify quality APIs that do not require a QGraph anymore.
committed
Pierre-Marie Pédrot
Stop unifying sorts in the kernel.
committed

November 2025

coqbot-app[bot]
Merge PR #21272: Instances-mod-elim-constraints
committed
Yann Leray
Instances mod elim (wrong graph)
committed

October 2025

coqbot-app[bot]
Merge PR #20506: An elimination constraint graph to manage elimination of sort variables
committed
Johann Rosain
Use elimination graph at elaboration
committed

September 2025

coqbot-app[bot]
Merge PR #21135: Remove Constr.isRefX from the API.
committed
Pierre-Marie Pédrot
Remove Constr.isRefX from the API.
committed

March 2025

coqbot-app[bot]
Merge PR #20351: Constr and HConstr: stop hashconsing in place
committed
Gaëtan Gilbert
Constr and HConstr: stop hashconsing in place
committed
coqbot-app[bot]
Merge PR #20344: Hashconsing try to avoid recomputing hashes
committed
Gaëtan Gilbert
Hashconsing try to avoid recomputing hashes
committed
coqbot-app[bot]
Merge PR #20340: Cleanup hashcons APIs and fix hashconsing of modpaths
committed
Gaëtan Gilbert
Cleanup hashcons APIs and fix hashconsing of modpaths
committed

January 2025

coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
committed

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
coqbot-app[bot]
Merge PR #19510: Constr.of_kind preserve more sharing
committed

September 2024

Gaëtan Gilbert
Constr.of_kind preserve more sharing
committed
Gaëtan Gilbert
Reorder destructor / constructor code in constr.ml
committed

July 2024

coqbot-app[bot]
Merge PR #19160: Avoid retypechecking repeated subterms in typeops
committed
Gaëtan Gilbert
Try to reuse partial hashconsing for definition bodies
committed
Gaëtan Gilbert
Avoid retypechecking repeated subterms in typeops
committed
Gaëtan Gilbert
constr hcons stats
committed

June 2024

coqbot-app[bot]
Merge PR #19202: hcons: remove `land 0x3FFFFFFF`
committed
coqbot-app[bot]
Merge PR #19170: Include constr hcons calls in profiling
committed
coqbot-app[bot]
Merge PR #19212: Don't skip [combinesmall 20] in Constr.
committed
Rodolphe Lepigre
Don't skip [combinesmall 20] in Constr.
committed
coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Statically enforce primitive string size invariant.
committed
Rodolphe Lepigre
Add a primitive string type.
committed
Gaëtan Gilbert
hcons: remove `land 0x3FFFFFFF`
committed
Gaëtan Gilbert
Include constr hcons calls in profiling
committed

May 2024

coqbot-app[bot]
Merge PR #18996: Remove the tag branch information from case_info.
committed