aboutsummaryrefslogtreecommitdiff
path: root/vernac/metasyntax.ml
AgeCommit message (Expand)Author
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
2018-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Change default for notations with variables bound to both terms and binders.Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20Notations: A step in cleaning constr_entry_key.Hugo Herbelin
2018-02-20Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Hugo Herbelin
2018-02-20More flexibility in locating or referring to a notation.Hugo Herbelin
2018-02-20Being more flexible on format Adding a warning to be more informativeHugo Herbelin
2018-02-20Respecting the ident/pattern distinction in notation modifiers.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20A bit of miscellaneous code documentation around notations.Hugo Herbelin
2018-02-20Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Hugo Herbelin
2018-02-20Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:59:04 +0000