coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of engine/univProblem.ml

April 2026

coqbot-app[bot]
Merge PR #21918: QLeq has nothing to do with elimination
committed
Yann Leray
QLeq has nothing to do with elimination
committed

January 2026

coqbot-app[bot]
Merge PR #21417: feat: Add elaboration of elimination constraints
committed
Tomas Diaz
feat: Add elim constraint elaboration
committed
coqbot-app[bot]
Merge PR #21471: Remove the QCumulConstraint type for good.
committed
Pierre-Marie Pédrot
Remove the QCumulConstraint type for good.
committed
coqbot-app[bot]
Merge PR #21459: Move sort cumulativity constraint types out of the kernel.
committed
Pierre-Marie Pédrot
Move sort cumulativity constraint types out of 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

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

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

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

February 2023

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

March 2022

coqbot-app[bot]
Merge PR #15863: Restrict the universe level algebra to a single small level.
committed
Pierre-Marie Pédrot
Remove Prop and SProp from the Level.t type.
committed
coqbot-app[bot]
Merge PR #15856: Remove the univ_of_sort function from the API.
committed
Pierre-Marie Pédrot
Invert the dependency between Sorts and UGraph.
committed
coqbot-app[bot]
Merge PR #15847: Remove the Prop < Set hack for template from the universe graph
committed
Pierre-Marie Pédrot
Remove Prop from the universe graph.
committed
coqbot-app[bot]
Merge PR #15837: Reduce Universe.t footprint
committed
Pierre-Marie Pédrot
Use Sorts.t instead of Universe.t in universe unification problems.
committed

July 2021

Pierre-Marie Pédrot
Merge PR #14626: Replace UnivProblem.to_constraints with [force] function
committed
Gaëtan Gilbert
Replace UnivProblem.to_constraints with [force] function
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed
Pierre-Marie Pédrot
Merge PR #14229: Normalize universes before comparing in progress
committed
Gaëtan Gilbert
Normalize universes before comparing in progress
committed

April 2021

Pierre-Marie Pédrot
Merge PR #14078: Remove unused UnivProblem.Set.subst_univs
committed
Gaëtan Gilbert
Remove unused UnivProblem.Set.subst_univs
committed
Pierre-Marie Pédrot
Merge PR #14042: Fix a bug in UnivProblem
committed

March 2021

Matthieu Sozeau
Fix a bug in UnivProblem
committed

July 2020

Maxime Dénès
Merge PR #10390: UIP in SProp
committed
Gaëtan Gilbert
UIP in SProp
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed

May 2018

Pierre-Marie Pédrot
Merge PR #7384: Split Universes
committed
Gaëtan Gilbert
Split off Universes functions about substitutions and constraints
committed