coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/term.ml

April 2026

coqbot-app[bot]
Merge PR #21859: More specific anomalies in contract_case
committed

March 2026

Gaëtan Gilbert
More specific anomalies in contract_case
committed

December 2025

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

April 2025

coqbot-app[bot]
Merge PR #20397: More uniform elimination management
committed
Johann Rosain
Kernel: removal of families, factorisation of elimination
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

July 2024

coqbot-app[bot]
Merge PR #19401: Annotate ocaml deprecations with the coq versions where they were deprecated
committed
Gaëtan Gilbert
Annotate ocaml deprecations with the coq versions where they were deprecated
committed

April 2024

coqbot-app[bot]
Merge PR #18867: Don't make Prop inductives template to control eliminator generation
committed
coqbot-app[bot]
Merge PR #18859: A few more list, context and term combinators
committed
Hugo Herbelin
Turn Declare.decompose into a standard "decompose_lambda_prod_n_decls" function.
committed
Gaëtan Gilbert
Term and EConstr.isArity don't substitute letins
committed

October 2023

coqbot-app[bot]
Merge PR #17947: An update to #15582: clarify remaining obscure points regarding decompose_{lambda,prod}{_n,}{_assum,_decls} functions
committed
Hugo Herbelin
Update on #15582: restore decompose_lambda_n_assum in Term as it is in EConstr.
committed

January 2023

coqbot-app[bot]
Merge PR #16903: Introduce sort variables in unification
committed
Pierre-Marie Pédrot
Extend the type of sort families to handle QSort.
committed
Pierre-Marie Pédrot
Introduce quality variables in sorts.
committed
coqbot-app[bot]
Merge PR #15582: Addressing proposal #15562: cleaning API of functions for destructing/constructing abstractions or products wrt contexts
committed

December 2022

Hugo Herbelin
Tentatively renaming prod_applist_assum & cie into prod_applist_decls
committed
Hugo Herbelin
Applying proposal #15562: uniformly-named iterated lambda/prod destructors.
committed

February 2022

coqbot-app[bot]
Merge PR #14727: Major refactoring of cooking.ml
committed
Hugo Herbelin
Adding Term.it_mkProd_wo_LetIn.
committed

January 2022

coqbot-app[bot]
Merge PR #15566: Errors from decompose_lam_n_assum & cie should be anomalies
committed
Hugo Herbelin
Turning user_err into anomaly in decompose_lam_n_assum and cie.
committed

October 2021

Pierre-Marie Pédrot
Merge PR #15003: Remove optional header in UserError
committed
Gaëtan Gilbert
Remove unused hdr argument of user_err
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

Enrico Tassi
Merge PR #11417: Move kind_of_type from the kernel to EConstr.
committed
Pierre-Marie Pédrot
Move kind_of_type from the kernel to ssr.
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
Maxime Dénès
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
committed
Guillaume Bertholon
Add primitive float computation in Coq kernel
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
Gaëtan Gilbert
Add a non-cumulative impredicative universe SProp.
committed
Gaëtan Gilbert
Make Sorts.t private
committed

February 2019

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

June 2018

Maxime Dénès
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
committed
Hugo Herbelin
Swapping Context and Constr: defining declarations on constr in Constr.
committed
Pierre-Marie Pédrot
Merge PR #7863: Remove Sorts.contents
committed
Gaëtan Gilbert
Remove Sorts.contents
committed