aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
Commit message (Expand)AuthorAge
* 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