aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
2015-12-25Fixing non exhaustive pattern-matching in 003fe3d5e60b.Hugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-21ARGUMENT EXTEND shares the toplevel representation when possible.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-10-28Type-safe Argextend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-25Getting rid of the Atactic entry.Pierre-Marie Pédrot
2015-10-25Getting rid of the Agram entry.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-19Record type for VERNAC EXTEND rules and a bit of documentation.Pierre-Marie Pédrot
2015-01-27Tentative fix for bug #3957.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-07Removing simple induction / destruct from the AST.Pierre-Marie Pédrot
2014-08-07Instead of relying on a trick to make the constructor tactic parse, putPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 04:01:17 +0000