aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacintern.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 dead code.Gravatar Pierre-Marie Pédrot2015-12-27
| |
* | 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.
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
|
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
| | | | | | | | | | | maybe ca71714). Goal 2=2+2. match goal with |- (_ = ?c) => simpl c end. was working in 8.4 but was failing in 8.5beta2. Note: Changes in tacintern.ml are otherwise purely cosmetic.
* Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Gravatar Pierre-Marie Pédrot2015-05-15
|
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
|
* 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.
* 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.
* 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.
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
| | | | at least when f is an evaluable reference.
* Hopefully the last word on having "simpl f" complying with theGravatar Hugo Herbelin2014-11-18
| | | | | | | semantics described in the reference manual (i.e. if "f" is a qualid, do not add implicit arguments and, a fortiori, do not try to solve these implicit arguments - in particular, changing DbLib which expected this rule not to be followed).
* 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
|
* Fixing #3562 ("as" in "destruct" expects either a disjunctiveGravatar Hugo Herbelin2014-11-07
| | | | intropattern or a bound ltac variable).
* 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.
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
| | | | | | being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine.
* 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.
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
| | | | as a disjunctive intropattern.
* 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.
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
|
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Code factorization in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 00:03:45 +0000