coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of interp/notation_ops.ml

October 2026

coqbot-app[bot]
Merge PR #19404: An algebra of types for the argument of notations
committed
Hugo Herbelin
More uniform naming in notation_ops.ml.
committed
Hugo Herbelin
Notation matching: separating clearly when a variable is a notation variable or not.
committed
Hugo Herbelin
A richer type system for notation variables.
committed
Hugo Herbelin
Looks like a typo in notation_ops.ml.
committed

March 2026

coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed

February 2026

coqbot-app[bot]
Merge PR #21574: Stop using genarg for constr syntax extension
committed
Gaëtan Gilbert
Stop using genarg for constr syntax extension
committed

November 2025

coqbot-app[bot]
Merge PR #21281: Pass printing flags functionally in constr printers
committed
Gaëtan Gilbert
Pass printing flags functionally in constr printers
committed
coqbot-app[bot]
Merge PR #21275: Stop looking at Printing Universes during externalisation
committed
Gaëtan Gilbert
Stop looking at Printing Universes during externalisation
committed

May 2025

coqbot-app[bot]
Merge PR #20609: Move print_parentheses ref to constrextern
committed
Gaëtan Gilbert
Move print_parentheses ref to constrextern
committed

February 2025

coqbot-app[bot]
Merge PR #20298: Locate on notation print additional info
committed
Gaëtan Gilbert
Locate on notation prints notation_location
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 #19481: Allow fast fresh name generation in detyping
committed

August 2024

Pierre-Marie Pédrot
Actually use the new fast map API in Detyping.
committed

July 2024

coqbot-app[bot]
Merge PR #19337: A few corner case notation bugs in the presence of binders
committed
Hugo Herbelin
Notation bug with too early use of alpha-conversion.
committed
Hugo Herbelin
Notation bug: missing check when a variable is both a binder and the term binding to this variable.
committed
Hugo Herbelin
Notation bug with let-in in binders used also as terms.
committed
Hugo Herbelin
Alpha-conversion notation bug.
committed

June 2024

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 #18981: Support syntax `Type@{q | _}`
committed

April 2024

Gaëtan Gilbert
Support syntax `Type@{q | _}`
committed

March 2024

coqbot-app[bot]
Merge PR #18763: Warn non-reversible-notation for notations using volatile casts
committed
Gaëtan Gilbert
Warn non-reversible-notation for notations using volatile casts
committed

December 2023

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

November 2023

coqbot-app[bot]
Merge PR #17856: Notation wish #17845: add support for notations with recursive binders involving "let" and "match"
committed
Hugo Herbelin
Support for printing (simple) notations with recursive binders in let/match.
committed
Hugo Herbelin
Generalize map_glob_constr_left_to_right with an action on binders.
committed
Hugo Herbelin
Generalize mk_glob_constr_eq wrt the treatment of binders.
committed
coqbot-app[bot]
Merge PR #17667: Support quotations (genargs) in patterns
committed
coqbot-app[bot]
Merge PR #18294: Introduce a dedicated type for evar kinds in raw / glob terms
committed
Gaëtan Gilbert
Move genarg substitutions to new pretyping/gensubst
committed
Pierre-Marie Pédrot
Merge the CHole / GHole naming information with the evar_kind.
committed
Pierre-Marie Pédrot
Split the evar_kinds type into one for evars and one for glob terms.
committed
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
coqbot-app[bot]
Merge PR #18104: Addresses #18096: more informative message when a notation cannot be intepreted as a reference
committed

October 2023

Hugo Herbelin
Exporting pr_notation_info in notation_ops.mli.
committed

September 2023

coqbot-app[bot]
Merge PR #17795: ComInductive universe computation cleanups
committed