aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacsubst.ml
Commit message (Collapse)AuthorAge
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
|
* Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there.
* 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
| | | | | | This was historically used together with the <:tactic< ... >> quotation to insert foreign code as $foo, but it actually only survived in the implementation of Tauto. With the removal of the quotation feature, this is now totally obsolete.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | | | The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv.
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant.
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
| | | | | | | | | | We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state.
* | 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
| | | | | | | | | | | | Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function.
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | 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
| |
* | Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
| |
* | Removing the globTacticIn primitive.Gravatar Pierre-Marie Pédrot2015-12-03
|/ | | | | It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee.
* Somehow fixing bug #3467.Gravatar Pierre-Marie Pédrot2015-02-27
| | | | | | The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly.
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
|
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main change is that selection of subterm is made similar whether the given term is fully applied or not. - The selection of subterm now works as follows depending on whether the "at" is given, of whether the subterm is fully applied or not, and whether there are incompatible subterms matching the pattern. In particular, we have: "at" given | subterm fully applied | | incompatible subterms | | | Y Y - it works like in 8.4 Y N - this was broken in 8.4 ("at" was ineffective and it was finding all subterms syntactically equal to the first one which matches) N Y Y it now finds all subterms like the first one which matches while in 8.4 it used to fail (I hope it is not a too risky in-draft for a semantics we would regret...) (e.g. "destruct (S _)" on goal "S x = S y + S x" now selects the two occurrences of "S x" while it was failing before) N Y N it works like in 8.4 N N - it works like in 8.4, selecting all subterms like the first one which matches - Note that the "historical" semantics, when looking for a subterm, to select all subterms that syntactically match the first subterm to match the pattern (looking from left to right) is now internally called "like first". - Selection of subterms can now find the type by pattern-matching (useful e.g. for "induction (nat_rect _ _ _ _)") - A version of Unification.w_unify w/o any conversion is used for finding the subterm: it could be easily replaced by an other matching algorithm. In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y". Secondary change is in the interpretation of terms with existential variables: - When several arguments are given, interpretation is delayed at the time of execution - Because we aim at eventually accepting "edestruct c" with unresolved holes in c, we need the sigma obtained from c to be an extension of the sigma of the tactics, while before, we just type-checked c independently of the sigma of the tactic - Finishing the resolution of evars (using type classes, candidates, pending conversion problems) is made slightly cleaner: it now takes three states: a term is evaluated in state sigma, leading to state sigma' >= sigma, with evars finally solved in state sigma'' >= sigma'; we solve evars in the diff of sigma' and sigma and report the solution in sigma'' - We however renounce to give now a success semantics to "edestruct c" when "c" has unresolved holes, waiting instead for a decision on what to do in the case of a similar eapply (see mail to coqdev). An auxiliary change is that an "in" clause can be attached to each component of a "destruct t, u, v", etc. Incidentally, make_abstraction does not do evar resolution itself any longer.
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
| | | | not draw Auto.
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* 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
|
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
|
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
| | | | | Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
* 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
| | | | | | | | | | 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.Gravatar Pierre-Marie Pédrot2014-08-07
|
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
|
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context).
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
| | | | subgoals and the role of the "by tac" clause swapped.
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | Differs from the usual t;[t1…tn] in two ways: * It can be used without a preceding tactic * It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals. In other words t;[t1…tn] is [> t;[>t1…tn].. ].
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:17:54 +0000