coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/uGraph.ml

May 2026

coqbot-app[bot]
Merge PR #22039: Remove the unused AcyclicGraph.choose primitive.
committed
Pierre-Marie Pédrot
Remove the unused AcyclicGraph.choose primitive.
committed
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

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 #21753: Fix subtyping with elim constraints
committed
Gaëtan Gilbert
Fix subtyping with elim constraints
committed

February 2026

coqbot-app[bot]
Merge PR #21531: Only allow universe level comparisons to fail with type-in-type
committed
Yann Leray
Only allow universe level comparisons to fail with type-in-type
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

December 2025

coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Add support for parsing elimination constraints
committed
Johann Rosain
Rename Constraint(s) to UnivConstraint(s) for a more consistent naming
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
Johann Rosain
Add the elimination constraint graph
committed

February 2025

coqbot-app[bot]
Merge PR #20178: Keep qvar in template poly entry and declarations
committed
Gaëtan Gilbert
Keep qvar in template poly entry
committed

January 2025

coqbot-app[bot]
Merge PR #19985: Stop using lbound:Prop
committed
Gaëtan Gilbert
Delete UGraph.Bound (now unused)
committed
coqbot-app[bot]
Merge PR #20102: Typecheck pseudo sort poly inductives in kernel using above prop qvar
committed
Gaëtan Gilbert
Typecheck pseudo sort poly inductives in kernel using above prop qvar
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

July 2024

coqbot-app[bot]
Merge PR #19311: Kernel: report all undeclared universes not just one
committed
Gaëtan Gilbert
Kernel: report all undeclared universes not just one
committed

June 2024

coqbot-app[bot]
Merge PR #19114: Using more often names of universes in universe inconsistency message, if possible
committed
Hugo Herbelin
Using more often names of universes in universe inconsistency message, if possible.
committed

February 2024

coqbot-app[bot]
Merge PR #18669: Fix misplaced attributes.
committed
Rodolphe Lepigre
Fix misplaced attributes.
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
sort poly (with simple squashing model and no inductive output in qsort)
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

May 2023

coqbot-app[bot]
Merge PR #17505: Turn "algebraic on the right" error into regular univ inconsistency
committed

April 2023

Gaëtan Gilbert
Turn "algebraic on the right" error into regular univ inconsistency
committed

March 2023

coqbot-app[bot]
Merge PR #17357: Understand type-in-type when checking (ie not infer) constraints
committed
Gaëtan Gilbert
Understand type-in-type when checking (ie not infer) constraints
committed

February 2023

coqbot-app[bot]
Merge PR #17177: Fix some universe name printing
committed
Gaëtan Gilbert
Fix some universe name printing
committed

January 2023

coqbot-app[bot]
Merge PR #17114: Remove the cumulative SProp flag.
committed
Pierre-Marie Pédrot
Remove the cumulative SProp flag.
committed
coqbot-app[bot]
Merge PR #16903: Introduce sort variables in unification
committed
Pierre-Marie Pédrot
Introduce quality variables in sorts.
committed

December 2022

coqbot-app[bot]
Merge PR #17016: Revert "Compat for serapi"
committed
Gaëtan Gilbert
Revert "Compat for serapi"
committed