aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_vernac.ml4
AgeCommit message (Expand)Author
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-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
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-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2017-03-23Factorizing/unifying code in dealing with binders.Hugo Herbelin
2017-03-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-16don't require printing-only notation to be productiveRalf Jung
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Fix #5174: Underinformative syntax error messages in the new arguments syntaxMaxime Dénès
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-03Merge remote-tracking branch 'github/pr/340' into v8.6Maxime Dénès
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-11-02Better Arguments compatibility.Maxime Dénès
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-06Do not add "Append" as a lexer keyword.Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Revert "Move bullet detection from lexer to parser (bug #5102)."Guillaume Melquiond
2016-10-04Merge remote-tracking branch 'github/pr/305' into v8.6Maxime Dénès
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Move bullet detection from lexer to parser (bug #5102).Guillaume Melquiond
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-07-26restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:56:51 +0000