coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/context.ml

June 2026

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
Move CompactedDecl to ppconstr
committed
coqbot-app[bot]
Merge PR #21982: Remove Context.Compacted.Declaration.to_named_context
committed

April 2026

Gaëtan Gilbert
Remove Context.Compacted.Declaration.to_named_context
committed

September 2025

coqbot-app[bot]
Merge PR #20957: Match-printing
committed
Yann Leray
Harmonise behaviour when inductives / constructors have local definitions and implicit arguments, as patterns
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 #19539: Context.map_annot{,_relevance}: make "smart", add _het version
committed
Gaëtan Gilbert
Context.map_annot_relevance: make "smart", add _het version
committed
Gaëtan Gilbert
Remove redundant internal Context.map_binder_relevance
committed

April 2024

coqbot-app[bot]
Merge PR #18938: Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
Gaëtan Gilbert
Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
coqbot-app[bot]
Merge PR #18859: A few more list, context and term combinators
committed
Hugo Herbelin
Adding map with relevance in context.ml.
committed

March 2024

coqbot-app[bot]
Merge PR #13445: Cleaning comAssumption.ml
committed
Hugo Herbelin
Adding more heterogeneous map functions in context.ml.
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

May 2023

coqbot-app[bot]
Merge PR #17466: typing.ml checks relevance annotations
committed
Gaëtan Gilbert
Typing.check_binder_relevance takes a reldecl
committed

March 2022

coqbot-app[bot]
Merge PR #15710: Three fixes in printing Record/Inductive (universe instances and mutual types)
committed
Hugo Herbelin
Adding a function Context.Rel.ids.
committed

February 2022

coqbot-app[bot]
Merge PR #15525: Make Scheme Equality compatible with universe polymorphism
committed

January 2022

Hugo Herbelin
Replace context_chop by a generic drop_lastn on contexts.
committed

September 2021

Pierre-Marie Pédrot
Merge PR #14794: Adding a few functions about rel context in constr and econstr together with a reorganization
committed

August 2021

Hugo Herbelin
Moving map_rel_context_with_binders to Context.Rel.
committed
coqbot-app[bot]
Merge PR #14726: Let Context.Named.to_instance conform to its specification + mini-simplifications about named_context
committed
Hugo Herbelin
Unifying terminology between Context.Rel and Context.Named.
committed
Hugo Herbelin
Fixing Context.Named.to_instance wrt its specification.
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed

November 2020

Pierre-Marie Pédrot
Merge PR #13397: Adding heterogeneous map on named contexts.
committed
Hugo Herbelin
Adding heterogeneous map on named contexts.
committed

March 2020

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

February 2020

Pierre-Marie Pédrot
Merge PR #11550: Fixing wrong comments in context.ml
committed
Hugo Herbelin
Fixing wrong comments in context.ml.
committed

November 2019

Gaëtan Gilbert
Merge PR #11010: [coq] Untabify the whole ML codebase.
committed
Emilio Jesus Gallego Arias
[coq] Untabify the whole ML codebase.
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

March 2019

Pierre-Marie Pédrot
Merge PR #8817: SProp: the definitionally proof irrelevant universe
committed
Gaëtan Gilbert
Add relevance marks on binders.
committed

February 2019

Pierre-Marie Pédrot
Merge PR #9317: Restrict universes in records.
committed

January 2019

Gaëtan Gilbert
Restrict universes in records.
committed

September 2018

Maxime Dénès
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
committed
Emilio Jesus Gallego Arias
[kernel] Compile with almost all warnings enabled.
committed

July 2018

Maxime Dénès
Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.
committed
Pierre-Marie Pédrot
Add combinators to drop the bodies of local declarations.
committed

June 2018

Maxime Dénès
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
committed