aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Expand)Author
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
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-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
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-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-19Print [uconstr] in genargs.Arnaud Spiwack
2014-11-19Proper printer for [uconstr] in [Pptactic].Arnaud Spiwack
2014-11-17Setting printing tags for Ltac.Pierre-Marie Pédrot
2014-11-17Moving printing code for red_expr and may_eval to Pptactic.Pierre-Marie Pédrot
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-05lib/RichPp: Rename into Richpp.Yann Régis-Gianas
2014-11-04printing/Ppannotation: New annotation for tactic syntactic objects.Regis-Gianas
2014-11-04printing/Pptactic.Make: New.Regis-Gianas
2014-11-01Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Arnaud Spiwack
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-12Replace the list of argument in tacexpr with a single row argument.Arnaud Spiwack
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-03Fixing printing of unreachable local tactics.Pierre-Marie Pédrot
2014-09-02Cleaning code in Pptactic.Pierre-Marie Pédrot
2014-09-02Removing [revert] tactic from the AST.Pierre-Marie Pédrot
2014-09-01Moving the decompose tactic out of the AST.Pierre-Marie Pédrot
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-12A couple of fixes/improvements in -beautify, but backtracking onHugo Herbelin
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
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-08-06Removing "intros untils" from the AST.Pierre-Marie Pédrot
2014-08-05Fixing a few beautifying bugs.Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-08-01Fix typo in cf04daec997.Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:20:36 +0000