coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/typeops.ml

June 2026

coqbot-app[bot]
Merge PR #22087: Move check_hyps_inclusion out of the kernel
committed
Gaëtan Gilbert
Move check_hyps_inclusion out of the kernel
committed
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
check_hyps_inclusion use variable status instead of conversion
committed
Gaëtan Gilbert
Keep track of variable status (secvar or not) in named contexts
committed

April 2026

coqbot-app[bot]
Merge PR #21883: Add test that the kernel checks relevances in Case binders
committed
Gaëtan Gilbert
Add test that the kernel checks relevances in Case binders
committed

March 2026

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

January 2026

coqbot-app[bot]
Merge PR #21533: Stop exposing implementation internals in Environ API.
committed
Pierre-Marie Pédrot
Stop exposing implementation internals in Environ API.
committed
coqbot-app[bot]
Merge PR #21508: Stop unifying sorts in the kernel.
committed
Pierre-Marie Pédrot
More precise type for UVar unification functions.
committed
coqbot-app[bot]
Merge PR #21459: Move sort cumulativity constraint types out of the kernel.
committed
Pierre-Marie Pédrot
Replace QCumulConstraints.t by ElimConstraints.t in kernel internals.
committed

December 2025

coqbot-app[bot]
Merge PR #21412: Clean up exceptions of recursion_scheme_error and pretype_errors
committed
Thomas Lamiaux
clean up exceptions of recursion_scheme_error
committed
coqbot-app[bot]
Merge PR #21380: Remove APIs that have been deprecated before 9.0.
committed
Pierre-Marie Pédrot
Remove APIs that have been deprecated before 9.0.
committed
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
Johann Rosain
Use elimination graph to manage elimination in the kernel
committed

September 2025

coqbot-app[bot]
Merge PR #21131: Proper error for projection type mismatch in Typeops.
committed
Pierre-Marie Pédrot
Proper error for projection type mismatch in Typeops.
committed
coqbot-app[bot]
Merge PR #21049: Check correctness of canonical constant and inductive names when typing.
committed
Pierre-Marie Pédrot
Check correctness of canonical constant and inductive names when typing.
committed

March 2025

coqbot-app[bot]
Merge PR #20303: Induction schemes refresh template universes
committed
Gaëtan Gilbert
instantiate_template_universes doesn't need a full mind_specif
committed

February 2025

coqbot-app[bot]
Merge PR #20178: Keep qvar in template poly entry and declarations
committed
Gaëtan Gilbert
Inductive.param_univs pass the entire default sort instead of the level
committed
coqbot-app[bot]
Merge PR #20165: Export a view type over Environ.env for Serlib and abstract env away.
committed

January 2025

Pierre-Marie Pédrot
Abstract away Environ.env.
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

November 2024

coqbot-app[bot]
Merge PR #19844: Typeops.type_of_apply fix empty stack check
committed
Gaëtan Gilbert
Typeops.type_of_apply fix empty stack check
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

September 2024

coqbot-app[bot]
Merge PR #19446: Reduce the Typeops API.
committed

August 2024

coqbot-app[bot]
Merge PR #19433: Hconstr tweak debug and profile printing
committed
Gaëtan Gilbert
HConstr.Tbl.create take unit not int
committed
Pierre-Marie Pédrot
Reduce the Typeops API.
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
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
Return HConstr.self in Typeops.infer judgment
committed
Gaëtan Gilbert
Avoid retypechecking repeated subterms in typeops
committed