aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/coretactics.ml4
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* 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
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
* 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
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* Removing symmetry from the atomic tactics.Gravatar Pierre-Marie Pédrot2014-06-02
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:00:27 +0000