aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-11
|\|
| * Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-10
|\|
| * Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
| * Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
| * Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:16:37 +0000