aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
* Fixing lexing of strings in comments for beautifier.Gravatar Hugo Herbelin2016-12-02
* Fix #5174: Underinformative syntax error messages in the new arguments syntaxGravatar Maxime Dénès2016-11-30
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* 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
|\
* | Removing obsolete parsing of strings à la v7 in comments.Gravatar Hugo Herbelin2016-11-05
* | 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 remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
|\
* \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \
| * | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
* | | Adding a primitive to recover the set of keywords from the lexer.Gravatar Pierre-Marie Pédrot2016-10-21
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ |/|
* | Extra warning about unicode character of unknown status following an ident.Gravatar Hugo Herbelin2016-10-17
* | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
* | Stopping warning on unrecognized unicode character in notation (fixing #5136).Gravatar Hugo Herbelin2016-10-17
* | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
* | More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
* | Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
* | Fix compilation with camlp4 broken in 8a8caba3.Gravatar Hugo Herbelin2016-10-17
|/
* Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
* Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
* Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* Do not add "Append" as a lexer keyword.Gravatar Pierre-Marie Pédrot2016-10-06
* Fix incorrect token description for bullets.Gravatar Guillaume Melquiond2016-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
|\
* | Move bullet detection from lexer to parser (bug #5102).Gravatar Guillaume Melquiond2016-10-02
| * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
|/
* Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\
* | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
* | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
|/
* Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* Silence the CAMLP5 warnings on command line.Gravatar Pierre-Marie Pédrot2016-09-02
* Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Gravatar Pierre Letouzey2016-07-26
* Removing useless grammar entries. Fixes bug #4919.Gravatar Pierre-Marie Pédrot2016-07-18
* Remove lexing of ordinal notations.Gravatar Maxime Dénès2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11Gravatar Pierre Letouzey2016-06-21