aboutsummaryrefslogtreecommitdiff
path: root/vernac/metasyntax.ml
AgeCommit message (Expand)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
2020-01-30Notations: Fixing a wrong location in format.Hugo Herbelin
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-09-10Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:24:01 +0000