aboutsummaryrefslogtreecommitdiff
path: root/vernac/metasyntax.ml
AgeCommit message (Expand)Author
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
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-09-25BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsPaul Steckler
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-18Fixing two anomalies in corner cases of the syntax of notation formats.Hugo Herbelin
2017-09-12Fixing bug #5693 (treating empty notation format as any format).Hugo Herbelin
2017-08-29Quoting notations in incompatible-level error message.Hugo Herbelin
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-01Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Maxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Adding support for recursive notations of the form "x , .. , y , z".Hugo Herbelin
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:33:00 +0000