coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/section.ml

October 2026

coqbot-app[bot]
Merge PR #22542: Replace and deprecate the aliased _env variants of Names sets and maps
committed

September 2026

Pierre-Marie Pédrot
Use the now correct set and maps Names APIs.
committed

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
Johann Rosain
Rename Constraint(s) to UnivConstraint(s) for a more consistent naming
committed

May 2025

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

April 2025

Kenji Maillard
Declare global sort variables
committed

February 2025

coqbot-app[bot]
Merge PR #20195: Stop relying on canonicalizing maps in the section mechanism.
committed
Pierre-Marie Pédrot
Stop relying on canonicalizing maps in the section mechanism.
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

April 2022

coqbot-app[bot]
Merge PR #15935: More compact representation for cooking_info
committed
Pierre-Marie Pédrot
Simplify the cooking API.
committed

February 2022

coqbot-app[bot]
Merge PR #15696: Simplify the Cooking API
committed
Pierre-Marie Pédrot
Abstract away some types in Cooking.
committed
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 #14654: A few terminology changes in module names of the universe API
committed
Hugo Herbelin
Renaming Univ.AUContext into Univ.AbstractContext.
committed
Hugo Herbelin
Renaming module Univ.Constraint into Univ.Constraints.
committed
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

May 2020

Pierre-Marie Pédrot
Merge PR #12344: Cleanup noisy prefixes
committed
Gaëtan Gilbert
Cleanup: remove noisy "sec_" prefixes in section.ml
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
Gaëtan Gilbert
Merge PR #10817: Remove redundancy in section hypotheses of kernel entries.
committed
Pierre-Marie Pédrot
Remove redundancy in section hypotheses of kernel entries.
committed
Pierre-Marie Pédrot
Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in sections
committed