coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of interp/notationextern.ml

October 2026

coqbot-app[bot]
Merge PR #19404: An algebra of types for the argument of notations
committed
Pierre Roux
Turn notation into a record
committed
Hugo Herbelin
A richer type system for notation variables.
committed
coqbot-app[bot]
Merge PR #22545: Implement deep %scope in Arguments
committed
Pierre Roux
[notation] Refactor internal representation of scopes stack
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

November 2025

coqbot-app[bot]
Merge PR #19177: [core] Improved state protection against memprof-limits interruptions
committed
Emilio Jesus Gallego Arias
[core] Improved state protection against memprof-limits interruptions
committed

September 2025

coqbot-app[bot]
Merge PR #21062: Stop relying on CanOrd in Notationextern.
committed
Pierre-Marie Pédrot
Stop relying on CanOrd in Notationextern.
committed

July 2025

coqbot-app[bot]
Merge PR #20857: Qualified names for custom entries
committed
Gaëtan Gilbert
Qualified names for custom entries
committed
coqbot-app[bot]
Merge PR #20843: Avoid Stdlib.compare in notation.ml
committed
Gaëtan Gilbert
Avoid Stdlib.compare in notation.ml
committed

December 2024

coqbot-app[bot]
Merge PR #19840: Delay import of notation sets in Notationextern.
committed

November 2024

Pierre-Marie Pédrot
Delay import of notation sets in Notationextern.
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 #19338: Trivial cleanup in notations
committed
Pierre-Marie Pédrot
Reduce the use of structural equality in Notationextern.
committed
Pierre-Marie Pédrot
Turn Notationextern.notation_rule into a record.
committed

February 2024

coqbot-app[bot]
Merge PR #18667: Remove notation-related API
committed
Pierre-Marie Pédrot
Move glob_prim_constr_key from Notationextern to Notation.
committed

January 2024

coqbot-app[bot]
Merge PR #18514: [nit] Use standard `Summary.ref` for regular Summary reference
committed
Emilio Jesus Gallego Arias
[nit] Use standard `Summary.ref` for regular Summary reference
committed

August 2023

coqbot-app[bot]
Merge PR #17827: Notations: collecting the notation variables binding in a given notation variable
committed

July 2023

Hugo Herbelin
Notations: compute the notation variables binding in a notation variable.
committed
coqbot-app[bot]
Merge PR #17115: Uniformizing the treatment of notations for terms and notations for "match"-patterns
committed
Hugo Herbelin
Make the internal interpretation of CPatNotation closer to CNotation.
committed
coqbot-app[bot]
Merge PR #17841: Fixes #15221: a case of invalid eta-expansion in notation printing
committed
Hugo Herbelin
Fixes #15221 part 1: notation with flexible head not a bounded application.
committed
coqbot-app[bot]
Merge PR #17823: Code cleanup in notations: use records instead of tuples for entries and subentries
committed
Hugo Herbelin
A notation cleanup suggested in #17117: using records in place of tuples.
committed

June 2023

coqbot-app[bot]
Merge PR #17605: Fix inverted logic in `Summary.ref ~local:true`
committed
coqbot-app[bot]
Merge PR #17117: Clarifying the logic of levels in custom and constr entry rules (reopening of #13025)
committed

May 2023

Hugo Herbelin
To make the treatment more uniform, we use levels also in constr.
committed
Hugo Herbelin
We introduce a type notation_entry_relative_level to preserve more informations about the subentries: we remember whether we are at any level, at the next level or at the self level.
committed
Gaëtan Gilbert
Fix inverted logic in `Summary.ref ~local:true`
committed

February 2023

coqbot-app[bot]
Merge PR #16937: Fixes #12467: internal inconsistency when a notation variable is used both for binder lists and for term lists
committed
Hugo Herbelin
Renaming AsNameOrPattern into AsAnyPattern to better reflect the role.
committed
Hugo Herbelin
Notations: reorganizing the conversion between parsing types and interp types.
committed

November 2022

coqbot-app[bot]
Merge PR #12324: Add command to disable notations
committed

October 2022

Hugo Herbelin
Adding a large inclusion order for notation interpretation.
committed
Hugo Herbelin
Adding support for deactivating/reactivating notations.
committed
Hugo Herbelin
Extracting a file notationextern.ml out of notation.ml.
committed