| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| | | |||
| * | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès | 2015-12-11 |
| | | |||
| * | Aliasing give_up with admit |  Enrico Tassi | 2015-03-22 |
| | | |||
| * | More expressive API for tclWITHHOLES. |  Pierre-Marie Pédrot | 2015-02-10 |
| | | |||
| * | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot | 2015-02-10 |
| | | | | | | | | This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics. | ||
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| | | |||
| * | A global [gfail] tactic which works like [fail] except that it fails even if ↵ |  Arnaud Spiwack | 2014-12-23 |
| | | | | | | | there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not. | ||
| * | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | 2014-12-16 |
| | | |||
| * | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | 2014-12-12 |
| | | | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | ||
| * | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack | 2014-10-22 |
| | | | | | The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function. | ||
| * | Removing [revert] tactic from the AST. | Pierre-Marie Pédrot | 2014-09-02 |
| | | |||
| * | Getting rid of atomic tactics in Tacenv. | Pierre-Marie Pédrot | 2014-08-31 |
| | | | | | | | ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement. | ||
| * | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-27 |
| | | | | | | | Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x] and we should try to reduce the use of this tactical, because it is mostly a legacy tactic. | ||
| * | Removing simple induction / destruct from the AST. | Pierre-Marie Pédrot | 2014-08-07 |
| | | |||
| * | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot | 2014-08-07 |
| | | | | | | | | | | | all the tactics using the constructor keyword in one entry. This has the side-effect to also remove the other variant of constructor from the AST. I also needed to hack around the "tauto" tactic to make it work, by calling directly the ML tactic through a TacExtend node. This may be generalized to get rid of the intermingled dependencies between this tactic and the infamous Ltac quotation mechanism. | ||
| * | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot | 2014-08-07 |
| | | |||
| * | Removing "intros untils" from the AST. | Pierre-Marie Pédrot | 2014-08-06 |
| | | |||
| * | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
| | | |||
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| | | |||
| * | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | 2014-06-06 |
| | | |||
| * | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | 2014-06-02 |
| | | |||
| * | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | 2014-05-22 |
| | | | | | variant of it, accepting an additional integer. | ||
| * | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | 2014-05-21 |
| | | |||
| * | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot | 2014-05-20 |
| | | |||
| * | Tactics declared through TACTIC EXTEND that are of the form | Pierre-Marie Pédrot | 2014-05-20 |
| | | | | | | | | | | "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node. | ||
| * | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | 2014-05-20 |
| | | | | | | | | | We eta-expand primitive Ltac functions, and instead of feeding TacExtend directly with its arguments, we use the environment to retrieve them. Some tactics from the AST were also moved away and made using this mechanism. | ||
| * | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | 2014-05-16 |
| "coretactics.ml4" file. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |