coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/section.mli

March 2026

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

December 2025

coqbot-app[bot]
Merge PR #21451: Additional safe guards around qualities in the kernel
committed
Pierre-Marie Pédrot
Do not allow declaring global sorts inside sections.
committed
coqbot-app[bot]
Merge PR #21391: Reintroduce Univ.ContextSet.t and fix kernel APIs to use it
committed
Pierre-Marie Pédrot
Fix kernel APIs to take Univ.ContextSet rather than the PConstraints one.
committed
coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Add support for parsing elimination constraints
committed

May 2025

coqbot-app[bot]
Merge PR #18615: Declare global sort variables
committed

April 2025

Kenji Maillard
Declare global sort variables
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 2022

coqbot-app[bot]
Merge PR #14727: Major refactoring of cooking.ml
committed
Hugo Herbelin
New file discharge.ml out of cooking.ml, allowing abstracting over cooking_info.
committed
Hugo Herbelin
Major refactoring of cooking.
committed
Hugo Herbelin
Small simplification of close_section.
committed

July 2021

coqbot-app[bot]
Merge PR #14692: Embedding user-side universes names in Univ.UContext
committed
Hugo Herbelin
Simplifying code by embedding names in Univ.UContext.
committed

June 2021

Pierre-Marie Pédrot
Merge PR #14417: Move cooking types to Declarations from Opaqueproof
committed
Gaëtan Gilbert
Move Section.abstr_info to Declarations, use in cooking_info
committed
Gaëtan Gilbert
Move cooking_info from Opaqueproof to Declarations
committed

April 2020

Pierre-Marie Pédrot
Merge PR #11972: Fix require in section
committed
Gaëtan Gilbert
Fix #11783 Require in Section
committed

March 2020

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

January 2020

Pierre-Marie Pédrot
Merge PR #11348: Discharge inductive types without rechecking them
committed
Gaëtan Gilbert
generate variance data for section universes (not yet used)
committed

December 2019

Pierre-Marie Pédrot
Merge PR #10829: Section.t is never empty
committed
Gaëtan Gilbert
Section.t is never empty
committed

October 2019

Pierre-Marie Pédrot
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
committed
Gaëtan Gilbert
Use kernel info from Global for Lib.sections_{depth,are_opened}
committed
Pierre-Marie Pédrot
Merge PR #10670: ComAssumption cleanup
committed
Gaëtan Gilbert
Remove "is_polymorphic_univ" checks in upper layers.
committed
Pierre-Marie Pédrot
Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in sections
committed
Gaëtan Gilbert
Loosen restrictions on mixing universe mono/polymorphism in sections
committed
Gaëtan Gilbert
Merge PR #10797: Implement discharging in kernel
committed

September 2019

Pierre-Marie Pédrot
Implement section discharging inside kernel.
committed
Maxime Dénès
Merge PR #10664: Putting sections libstack inside the kernel
committed
Pierre-Marie Pédrot
Move the Lib section data into the kernel.
committed