aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/tacexpr.mli
Commit message (Expand)AuthorAge
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
* Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
* Expliciting the fact that the atomic tactic type is self-contained.Gravatar Pierre-Marie Pédrot2016-04-10
* Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
* Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Removing the MetaIdArg entry of tactic expressions.Gravatar Pierre-Marie Pédrot2016-02-24
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* | 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
* | 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-02-10
|\|
| * Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* | 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
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01