aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Remove other types not carried by interpretations in `Tacexpr`.Gravatar Arnaud Spiwack2015-06-25
* Remove useless `and_short_name` in interpreted level in `Tacexpr`.Gravatar Arnaud Spiwack2015-06-25
* 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
* | 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
* | Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-18
| * Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
|/
* 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
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Print [uconstr] in genargs.Gravatar Arnaud Spiwack2014-11-19
* Proper printer for [uconstr] in [Pptactic].Gravatar Arnaud Spiwack2014-11-19
* Setting printing tags for Ltac.Gravatar Pierre-Marie Pédrot2014-11-17
* Moving printing code for red_expr and may_eval to Pptactic.Gravatar Pierre-Marie Pédrot2014-11-17
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
* printing/Pptactic.Make: New.Gravatar Regis-Gianas2014-11-04
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Fixing printing of unreachable local tactics.Gravatar Pierre-Marie Pédrot2014-09-03
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Fixing a few beautifying bugs.Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 00:17:52 +0000