aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
Commit message (Expand)AuthorAge
* Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Gravatar Maxime Dénès2017-08-29
|\
* | Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
* | Change the option for cumulativityGravatar Amin Timany2017-07-31
| * [general] Remove spurious dependency of highparsing on toplevel.Gravatar Emilio Jesus Gallego Arias2017-07-31
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)Gravatar Pierre Letouzey2017-06-14
* [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
|\
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\ \
| | | * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |/ | |/|
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [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
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \
| | * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
| |/ |/|
* | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \
* | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| * | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ /
| * Factorizing/unifying code in dealing with binders.Gravatar Hugo Herbelin2017-03-23
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
| * don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix #5174: Underinformative syntax error messages in the new arguments syntaxGravatar Maxime Dénès2016-11-30
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| * \ Merge remote-tracking branch 'github/pr/340' into v8.6Gravatar Maxime Dénès2016-11-03
| |\ \
| | | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| * | | Better Arguments compatibility.Gravatar Maxime Dénès2016-11-02
| | |/ | |/|
| | * Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\|
| * Do not add "Append" as a lexer keyword.Gravatar Pierre-Marie Pédrot2016-10-06
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Revert "Move bullet detection from lexer to parser (bug #5102)."Gravatar Guillaume Melquiond2016-10-05
| * Merge remote-tracking branch 'github/pr/305' into v8.6Gravatar Maxime Dénès2016-10-04
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Move bullet detection from lexer to parser (bug #5102).Gravatar Guillaume Melquiond2016-10-02