aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_tactic.ml4
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
* | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
| |
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* | 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
| |
* | 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
| |
* | Removing unused parsing entries.Gravatar Pierre-Marie Pédrot2015-12-28
| |
* | 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.
* | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
| | | | | | | | | | to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction".
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
| |
* | Tactics: Generalizing the use of the experimental clearing modifier toGravatar Hugo Herbelin2015-12-15
|/ | | | all cases of rewrite.
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | Marking it as experimental.
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
| | | | | | | | based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal.
* Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
| | | | | | pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though.
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
|
* Manually expand red_tactic so that notations do not break reduction tactics. ↵Gravatar Guillaume Melquiond2015-10-30
| | | | (Fix bug #3654)
* Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Gravatar Guillaume Melquiond2015-10-29
| | | | | Without this expansion, camlp4 fails to properly factor a user notation starting with either "trivial" or "auto".
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
| | | | This is necessary to make ssr compile with both camlp4/5
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
| | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
* 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
|
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
|
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
| | | | | | clause; extended it so that an induction over "x" is considered generic when the clause has the form "in H |-" (w/o the conclusion) and x does not occur in the conclusion.
* Dead codeGravatar Hugo Herbelin2014-10-27
|
* 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.
* 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.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
| | | | as a disjunctive intropattern.
* 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
|
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
* 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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 23:41:13 +0000