| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-17 | Removing the special status of generic arguments defined by Coq itself. | Pierre-Marie Pédrot | |
| This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. | |||
| 2016-03-17 | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot | |
| The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. | |||
| 2016-03-04 | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations]. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "move" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "exists" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "symmetry" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "generalize dependent" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clearbody" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clear" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "cofix" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "fix" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2015-12-27 | Tentative API fix for tactic arguments to be fed to tclWITHHOLES. | Pierre-Marie Pédrot | |
| The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. | |||
| 2015-12-25 | Moving specialize to Proofview.tactic. | Hugo Herbelin | |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-21 | Changing the toplevel type of the int_or_var generic type to int. | Pierre-Marie Pédrot | |
| 2015-12-11 | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès | |
| 2015-03-22 | Aliasing give_up with admit | Enrico Tassi | |
| 2015-02-10 | More expressive API for tclWITHHOLES. | Pierre-Marie Pédrot | |
| 2015-02-10 | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot | |
| This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics. | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ↵ | Arnaud Spiwack | |
| 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. | |||
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | |
| You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | |||
| 2014-10-22 | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack | |
| 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. | |||
| 2014-09-02 | Removing [revert] tactic from the AST. | Pierre-Marie Pédrot | |
| 2014-08-31 | Getting rid of atomic tactics in Tacenv. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-08-27 | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-08-07 | 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 | |
| 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. | |||
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot | |
| 2014-08-06 | Removing "intros untils" from the AST. | Pierre-Marie Pédrot | |
| 2014-08-01 | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-06 | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | |
| 2014-06-02 | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | |
| 2014-05-22 | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | |
| variant of it, accepting an additional integer. | |||
| 2014-05-21 | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | |
| 2014-05-20 | 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 | |
| "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. | |||
| 2014-05-20 | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | |
| "coretactics.ml4" file. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |