aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
| |\
| * | Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
| | * Fixing #4970 (confusion between special "{" and non special "{{" in notations).Gravatar Hugo Herbelin2016-10-03
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
* | | Allowing to extend the Print Grammar command generically.Gravatar Pierre-Marie Pédrot2016-09-14
* | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Properly handle the only printing flag in Reserved Notations.Gravatar Pierre-Marie Pédrot2016-06-28
* | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
* | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
* | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \ \ | | |/ | |/|
| * | Tentatively fixing misguiding error message with "binder" type inGravatar Hugo Herbelin2016-06-13
| | * Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| | * Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
| |/ |/|
| * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Properly handle notations containing spaces (bug #4538).Gravatar Guillaume Melquiond2016-05-02
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* | Was too restrictive in syntactic definitions, not imagining that theyGravatar Hugo Herbelin2016-03-28
* | Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
* | Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
* | Relying on parsing rules rather than genarg to check if an argument is empty.Gravatar Pierre-Marie Pédrot2016-03-17
* | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
* | Infering atomic ML entries from their grammar.Gravatar Pierre-Marie Pédrot2016-02-01
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Type-safe Egramml.grammar_prod_item.Gravatar Pierre-Marie Pédrot2015-10-27
* | Finer type for Pcoq.interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
* | Indexing existentially quantified entries returned by interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
* | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\|
| * Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:22:47 +0000