coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/typeops.mli

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

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

Pierre-Marie Pédrot
Reduce the Typeops API.
committed

July 2024

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

June 2024

coqbot-app[bot]
Merge PR #19164: Stop repairing bad relevances in the kernel
committed
Gaëtan Gilbert
Stop repairing bad relevances in the kernel
committed
coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Statically enforce primitive string size invariant.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

May 2024

coqbot-app[bot]
Merge PR #19071: Slight comment update after empty matches got CaseInvert
committed
Gaëtan Gilbert
Slight comment update after empty matches got CaseInvert
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 #18864: Call guard checking with evar handlers in higher layers
committed

March 2024

Gaëtan Gilbert
Monomorphize cclosure.evar_handler
committed

November 2023

coqbot-app[bot]
Merge PR #18340: Fix const_relevance and default qvar handler with sort polymorphism
committed
Gaëtan Gilbert
Move evar_handler type to cclosure and make evar_handler argument implicit
committed
coqbot-app[bot]
Merge PR #18280: Move relevance outside of case_info
committed
Gaëtan Gilbert
Move relevance outside of case_info
committed
coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

May 2023

coqbot-app[bot]
Merge PR #17585: Revised warning API: warnings can have multiple categories
committed
Gaëtan Gilbert
Use new warning API to provide nicer printer for bad relevance warning
committed
coqbot-app[bot]
Merge PR #17466: typing.ml checks relevance annotations
committed
Gaëtan Gilbert
typing.ml checks relevance annotations
committed

January 2023

coqbot-app[bot]
Merge PR #17140: Better messages for kernel qualities and relevance errors
committed
Pierre-Marie Pédrot
Intercept bad relevance warnings in Typeops and turn them into errors.
committed

September 2022

coqbot-app[bot]
Merge PR #16480: Generalize kernel evar handling
committed
Pierre-Marie Pédrot
Wrap the evar expander type into an explicit record.
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

May 2021

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

January 2021

coqbot-app[bot]
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
committed
Pierre-Marie Pédrot
Change the representation of kernel case.
committed

October 2020

coqbot-app[bot]
Merge PR #13151: Remove the compare_graph field from the conversion API.
committed
Pierre-Marie Pédrot
Similarly remove the explicit graph argument in the ~evar conversion API.
committed

July 2020

Pierre-Marie Pédrot
Merge PR #11604: Primitive persistent arrays
committed
Maxime Dénès
Primitive persistent arrays
committed
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

February 2020

Pierre-Marie Pédrot
Merge PR #11544: Cleanup some globref related manipulations
committed
Gaëtan Gilbert
ReferenceVariables error contains a globref instead of a constr
committed