coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of interp/implicit_quantifiers.ml

October 2026

coqbot-app[bot]
Merge PR #19404: An algebra of types for the argument of notations
committed
Hugo Herbelin
A richer type system for notation variables.
committed

August 2026

coqbot-app[bot]
Merge PR #22372: Abstract away the Summary reference type.
committed
Pierre-Marie Pédrot
Abstract away the Summary reference type.
committed

September 2025

coqbot-app[bot]
Merge PR #21020: Add an API for canonicalizing maps in Environ.
committed

August 2025

Pierre-Marie Pédrot
Canonicalize the GlobRef map API from Typeclasses.
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

December 2023

coqbot-app[bot]
Merge PR #18143: Debug printing for relevance marks
committed
Gaëtan Gilbert
Debug printing for relevance marks
committed

May 2023

coqbot-app[bot]
Merge PR #17585: Revised warning API: warnings can have multiple categories
committed
coqbot-app[bot]
Merge PR #17633: Move Termops.decompose_app_vect to EConstr, rename decompose_app->decompose_app_list, decompose_app_vect->decompose_app
committed
Gaëtan Gilbert
Remove low-value warning categories
committed
Gaëtan Gilbert
Revised warning API: warnings can have multiple categories
committed
Gaëtan Gilbert
Rename decompose_app->decompose_app_list, decompose_app_vect->decompose_app
committed

March 2023

coqbot-app[bot]
Merge PR #17283: More careful handling of possibly universe polymorphic globrefs
committed
Gaëtan Gilbert
Typeclasses.class_info and instances return option
committed

December 2021

coqbot-app[bot]
Merge PR #15317: Libobject/Lib name handling refactor
committed
Gaëtan Gilbert
Leaf objects do not need a low level id
committed
Gaëtan Gilbert
Substitutivity is a variant (no contents)
committed
Gaëtan Gilbert
Most objects don't care about names
committed

October 2021

coqbot-app[bot]
Merge PR #15005: Add periods to error messages
committed
alizter.tngl.sh
Add periods to error messages.
committed
Pierre-Marie Pédrot
Merge PR #15003: Remove optional header in UserError
committed
Gaëtan Gilbert
Remove unused hdr argument of user_err
committed

August 2021

Pierre-Marie Pédrot
Merge PR #14817: A few miscellaneous typos
committed
Hugo Herbelin
Missing period in an error message.
committed
Pierre-Marie Pédrot
Merge PR #14598: Explicit Projection nodes in concrete syntax
committed

July 2021

Hugo Herbelin
Introducing specific constructors for projections in constr_expr, glob_term.
committed

November 2020

coqbot-app[bot]
Merge PR #13132: Understand Mangle Names in implicit generalization
committed

October 2020

Pierre-Marie Pédrot
Merge PR #13118: [type classes] Simplify cl_context
committed
Gaëtan Gilbert
Remove unused is_class info from cl_context
committed
Gaëtan Gilbert
Implicit_quantifiers don't use precomputed is_class data
committed
Gaëtan Gilbert
Simplify Implicit_quantifiers.combine_params a bit
committed
Gaëtan Gilbert
First list in cl_context is just booleans
committed
Gaëtan Gilbert
Understand Mangle Names in implicit generalization
committed

July 2020

Gaëtan Gilbert
Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in custom gr…
committed
Maxime Dénès
Fix #11121: Simultaneous definition of term and notation in custom grammar
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

Emilio Jesus Gallego Arias
Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation
committed
Hugo Herbelin
Addressing #6082 and #7766 (overriding format of notation).
committed
Hugo Herbelin
Merge PR #11235: Add syntax for non maximal implicit arguments
committed
SimonBoulier
Add syntax for non maximally inserted implicit arguments
committed

November 2019

Emilio Jesus Gallego Arias
Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder
committed
Gaëtan Gilbert
Merge PR #11010: [coq] Untabify the whole ML codebase.
committed
Emilio Jesus Gallego Arias
[coq] Untabify the whole ML codebase.
committed
Hugo Herbelin
Fixing bugs in the computation of implicit arguments for fix with a let binder.
committed

August 2019

Gaëtan Gilbert
Merge PR #10665: [api] Move handling of variable implicit data to impargs
committed
Emilio Jesus Gallego Arias
[api] Move handling of variable implicit data to impargs
committed