coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/qGraph.ml

May 2026

coqbot-app[bot]
Merge PR #22014: Special handling of root node in AcyclicGraph algorithm
committed
Pierre-Marie Pédrot
Allow setting a root in AcyclicGraph.
committed

April 2026

coqbot-app[bot]
Merge PR #21885: Validate Proof: detect missing constraints, error if any issues found
committed
Gaëtan Gilbert
Validate Proof: detect missing constraints, error if any issues found
committed

March 2026

coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed

February 2026

coqbot-app[bot]
Merge PR #21531: Only allow universe level comparisons to fail with type-in-type
committed
Yann Leray
Add ignore_elimination_constraints typing flag
committed

January 2026

coqbot-app[bot]
Merge PR #21508: Stop unifying sorts in the kernel.
committed
Pierre-Marie Pédrot
Stop unifying sorts in the kernel.
committed
coqbot-app[bot]
Merge PR #21417: feat: Add elaboration of elimination constraints
committed
coqbot-app[bot]
Merge PR #21506: Equi-eliminability of sorts does not imply equality anymore.
committed
Tomas Diaz
feat: Add elim constraint elaboration
committed
Tomas Diaz
print: Add printing of elimination constraints for UState
committed
coqbot-app[bot]
Merge PR #21504: Fix spacing in qgraph error message
committed
Pierre-Marie Pédrot
Equi-eliminability of sorts does not imply equality anymore.
committed
Gaëtan Gilbert
Fix spacing in qgraph error message
committed
coqbot-app[bot]
Merge PR #21501: Various fixes around bound universe instances in kernel and checker
committed
Pierre-Marie Pédrot
Refine the declaredness criterion for qualities in kernel.
committed
coqbot-app[bot]
Merge PR #21486: Remove the coupling between sort constraint addition and rigidity check
committed
Pierre-Marie Pédrot
Move constraint_source from QGraph to UState.
committed
Pierre-Marie Pédrot
Split rigidity check from quality constraint addition.
committed

December 2025

coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Add bug files of stuff actually tested using elimination constraints
committed
Johann Rosain
Add support for parsing elimination constraints
committed

November 2025

coqbot-app[bot]
Merge PR #21272: Instances-mod-elim-constraints
committed
Yann Leray
Have a more useful Environ.set_qualities
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
Johann Rosain
Use elimination graph to manage elimination in the kernel
committed
Johann Rosain
Add the elimination constraint graph
committed