aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/tacexpr.mli
Commit message (Collapse)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
|
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
| | | | | | Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
* Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* 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
| | | | | | 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.
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
| | | | | | This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877.
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
| | | | [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
* 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.
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
|
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01
| | | | | | | | | | Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong. It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour). A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted. Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).
* 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.
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
| | | | as a disjunctive intropattern.
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
| | | | | | This has several benefits * It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages. * It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr]. * More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier.
* 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
|
* Removing the 'inductive' parameter from tacexpr AST.Gravatar Pierre-Marie Pédrot2014-09-01
| | | | | It was actually useless, because its only use was in the moved away decompose tactic.
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
|
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
* 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 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].. ].
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
|
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
|
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
| | | | | | It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
| | | | potentially conflicting tactics names from different plugins.
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
|
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
| | | They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
| | | | the checker, and it was not used before that anyway.
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
| | | | | | | This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP.
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
|
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
| | | | variant of it, accepting an additional integer.
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
|
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
|
* 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
|
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-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 dedicatedGravatar Pierre-Marie Pédrot2014-05-16
| | | | "coretactics.ml4" file.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:12:57 +0000