aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
* Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
* Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:27:24 +0000