aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* 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
|\|
| * Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| * Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 20:43:22 +0000