aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
Commit message (Expand)AuthorAge
* 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
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 11:37:32 +0000