coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of interp/notation.mli

October 2026

coqbot-app[bot]
Merge PR #19404: An algebra of types for the argument of notations
committed
Hugo Herbelin
A few comments about the API of notations.
committed
Pierre Roux
Fold notation
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] Implement deep %scope in Arguments
committed
Pierre Roux
[notation] Refactor internal representation of scopes stack
committed

July 2026

coqbot-app[bot]
Merge PR #22194: Add (more) location information to notations.
committed
Johannes Hostert
add location notation information
committed

March 2026

coqbot-app[bot]
Merge PR #21719: Notation.interp_prim_token does not need to return the scope
committed
Gaëtan Gilbert
Notation.interp_prim_token does not need to return the scope
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

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 Notation.
committed

July 2025

coqbot-app[bot]
Merge PR #20926: Split some primitive notation code from notation.ml
committed
Gaëtan Gilbert
Split some primitive notation code from notation.ml
committed
coqbot-app[bot]
Merge PR #20911: Make type Notation.prim_token_uid private
committed
Gaëtan Gilbert
Make type Notation.prim_token_uid private
committed
coqbot-app[bot]
Merge PR #20857: Qualified names for custom entries
committed
Gaëtan Gilbert
Qualified names for custom entries
committed

May 2025

coqbot-app[bot]
Merge PR #20107: Allow error messages from number/string notation parsers
committed
coqbot-app[bot]
Merge PR #20600: Fix missing implicit name from notation ToPostHole
committed
Gaëtan Gilbert
Fix missing implicit name from notation ToPostHole
committed

April 2025

Gaëtan Gilbert
Allow error messages from string notation parsers
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

December 2024

coqbot-app[bot]
Merge PR #19530: Give Stdlib its own directory
committed
Pierre Roux
Use Corelib instead of Stdlib as namespace for rocq-core
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 #19310: Rename Coq requirement prefix to Stdlib
committed
Pierre Roux
Renaming Coq -> Stdlib
committed

June 2024

coqbot-app[bot]
Merge PR #19075: Make CSet extensible on our side, and adding CSet.List.union.
committed
coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed
Hugo Herbelin
Make CSet extensible on our side, and adding Set.List.union.
committed

May 2024

coqbot-app[bot]
Merge PR #18714: Ltac2 `assert` scope: intern and typecheck types as types
committed

April 2024

Gaëtan Gilbert
Ltac2 `assert` scope: intern and typecheck types as types
committed

March 2024

coqbot-app[bot]
Merge PR #18739: Fixes "where notation" clause of interactive Fixpoint
committed
Hugo Herbelin
Fixes "where notation" clause of interactive Fixpoint.
committed

February 2024

coqbot-app[bot]
Merge PR #18667: Remove notation-related API
committed
Pierre-Marie Pédrot
Remove primitive token API discouraged since 2018.
committed
coqbot-app[bot]
Merge PR #18248: Generalize the deprecation machinery to other forms of comments
committed
Pierre Roux
Activate warn attribute for notations
committed

January 2024

coqbot-app[bot]
Merge PR #18443: Granting wish #18097: Print and About see through abbreviations playing the role of aliases
committed
Hugo Herbelin
Display also the body of the notation in Print/About on a notation.
committed
coqbot-app[bot]
Merge PR #18447: Fixes #18342: try to insert an entry coercion when a notation in a custom entry has arguments
committed

December 2023

Hugo Herbelin
Fixes #18342: try insert entry coercion to constr in applied custom notations.
committed

November 2023

coqbot-app[bot]
Merge PR #18104: Addresses #18096: more informative message when a notation cannot be intepreted as a reference
committed