aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Expand)AuthorAge
...
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
* | Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Fixing non exhaustive pattern-matching in 003fe3d5e60b.Gravatar Hugo Herbelin2015-12-25
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | ARGUMENT EXTEND shares the toplevel representation when possible.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
* | Type-safe Argextend.Gravatar Pierre-Marie Pédrot2015-10-28
* | 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
* | Type-safe grammar extensions.Gravatar Pierre-Marie Pédrot2015-10-27
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
* | Getting rid of the Atactic entry.Gravatar Pierre-Marie Pédrot2015-10-25
* | Getting rid of the Agram entry.Gravatar Pierre-Marie Pédrot2015-10-25
* | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * A more user-friendly naming of variables of ltac names defined byGravatar Hugo Herbelin2015-05-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-23
|\|
| * Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
| * Record type for VERNAC EXTEND rules and a bit of documentation.Gravatar Pierre-Marie Pédrot2015-02-19
* | Tentative fix for bug #3957.Gravatar Pierre-Marie Pédrot2015-01-27
* | Splitting ML tactics in one function per grammar entry.Gravatar Pierre-Marie Pédrot2015-01-23
* | 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
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Continuing 3741c46fe134 on reporting ltac error.Gravatar Hugo Herbelin2014-11-08
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 22:07:33 +0000