coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of interp/notation.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] Implement deep %scope in Arguments
committed
Pierre Roux
[notation] Refactor internal representation of scopes stack
committed
Pierre Roux
[notation] Use a record for arguments_scope_obj
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

July 2026

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

May 2026

coqbot-app[bot]
Merge PR #22010: Fix nametab handling when printing abbreviation
committed
Gaëtan Gilbert
Fix nametab handling when printing abbreviation
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

January 2026

coqbot-app[bot]
Merge PR #21511: Improve "Unknown interpretation for notation" error message
committed
Gaëtan Gilbert
Improve "Unknown interpretation for notation" error message
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 #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 #21016: Extend and cleanup the abbreviation API.
committed
Rodolphe Lepigre
Extend and cleanup the abbreviation API.
committed
coqbot-app[bot]
Merge PR #21062: Stop relying on CanOrd in Notationextern.
committed
coqbot-app[bot]
Merge PR #21040: Provide canonical map APIs in Environ.QConstant etc
committed
Pierre-Marie Pédrot
Stop relying on CanOrd in Notationextern.
committed
Gaëtan Gilbert
Provide canonical map APIs in Environ.QConstant etc
committed
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
coqbot-app[bot]
Merge PR #20843: Avoid Stdlib.compare in notation.ml
committed
Gaëtan Gilbert
Avoid Stdlib.compare in notation.ml
committed

June 2025

coqbot-app[bot]
Merge PR #20787: Simplify some uses of pr_global_env
committed
coqbot-app[bot]
Merge PR #20774: Fix returning delimiter instead of scope name for About in specific scope
committed
Quentin Corradi
simplify uses of pr_global_env
committed
Gaëtan Gilbert
Fix returning delimiter instead of scope name for About in specific scope
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
Evar kind ImplicitArg always contains an ident
committed
Gaëtan Gilbert
Fix missing implicit name from notation ToPostHole
committed
coqbot-app[bot]
Merge PR #18615: Declare global sort variables
committed

April 2025

Gaëtan Gilbert
Rename UnivGen.fresh_sort_quality to fresh_sort_in_quality
committed
coqbot-app[bot]
Merge PR #20565: lib.ml reduce dependence on Global
committed
Gaëtan Gilbert
lib.ml reduce dependence on Global
committed
coqbot-app[bot]
Merge PR #20397: More uniform elimination management
committed