coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of plugins/syntax/number_string.ml

September 2026

coqbot-app[bot]
Merge PR #22526: Reduce the equality APIs in Constr
committed
Pierre-Marie Pédrot
Remove Constr.eq_constr_nounivs.
committed

April 2026

coqbot-app[bot]
Merge PR #21863: Move the dubious compare and hash functions from Constr to a Termops submodule
committed
Pierre-Marie Pédrot
Move the dubious compare and hash functions from Constr to a Termops submodule.
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

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

June 2025

coqbot-app[bot]
Merge PR #20787: Simplify some uses of pr_global_env
committed
Quentin Corradi
simplify uses of pr_global_env
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
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 #20397: More uniform elimination management
committed
Johann Rosain
Kernel: removal of families, factorisation of elimination
committed
Gaëtan Gilbert
Number/String notations tolerate unregistered sum and option types
committed
Gaëtan Gilbert
Allow error messages from string notation parsers
committed

March 2025

Gaëtan Gilbert
Simplify target identification in number/string notation declaration
committed
Gaëtan Gilbert
Number notation: Stop returning unused values in locate_number
committed

October 2024

coqbot-app[bot]
Merge PR #19743: Rocqify Coqlib
committed
Pierre-Marie Pédrot
Rename the Coqlib module into Rocqlib.
committed
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

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed
Rodolphe Lepigre
Uniform handling of numbers and strings in [plugin/syntax].
committed
Rodolphe Lepigre
Combine string and numbers in [plugin/syntax].
committed