aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
Commit message (Expand)AuthorAge
* Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\
* | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| * Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
|/
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
* Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
* More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
* Being more flexible on format Adding a warning to be more informativeGravatar Hugo Herbelin2018-02-20
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
* Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Gravatar Hugo Herbelin2018-02-20
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
* \ Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Gravatar Maxime Dénès2017-10-09
|\ \
| | * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
| |/ |/|
| * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
* | Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \
* | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| |/ |/|
| * Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
| * Fixing two anomalies in corner cases of the syntax of notation formats.Gravatar Hugo Herbelin2017-09-18
|/
* Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
* Quoting notations in incompatible-level error message.Gravatar Hugo Herbelin2017-08-29
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Gravatar Maxime Dénès2017-08-01
|\
* | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| * Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 20:59:51 +0000