aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Tacinterp: [interp_message] and associate now only require an environment ↵Gravatar Arnaud Spiwack2014-08-05
| | | | rather than an entire goal.
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
| | | | | When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal. I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
* Fix interpretation bug in [uconstr].Gravatar Arnaud Spiwack2014-08-05
| | | Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac].
* The [refine] tactic now accepts [uconstr].Gravatar Arnaud Spiwack2014-08-05
| | | Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
| | | | | | | | | * Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v
* Move to a representation of universe polymorphic constants using indices for ↵Gravatar Matthieu Sozeau2014-08-03
| | | | | | | variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside.
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
|
* Faster uconstr.Gravatar Arnaud Spiwack2014-08-01
| | | Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
* 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 [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | | The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails. Together with [numgoal] can be used to fork on the number of goals of a tactic. The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
|
* Untyped terms in ltac: simplify [coerce_to_uconstr].Gravatar Arnaud Spiwack2014-08-01
| | | | Following advice by Hugo Herbelin.
* Remove spurious [1] in equality.ml.Gravatar Arnaud Spiwack2014-08-01
| | | | Introduced in a4043608f
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
| | | | catched otherwise due to the discrepancy between evars and metas.
* Fix discrimination net which was not recognizing primitive projections.Gravatar Matthieu Sozeau2014-07-30
|
* Untyped terms in tactic: add the possibility to use a typed term inside an ↵Gravatar Arnaud Spiwack2014-07-29
| | | | untyped term.
* 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.
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
|
* CPS-style tactic matching. We use the tactic monad as the target of the CPS.Gravatar Pierre-Marie Pédrot2014-07-28
| | | | | This allows for tail-rec calls, prevents unwanted capture of closures and results in an overall more efficient evaluation.
* Code cleaning in Tacenv.Gravatar Pierre-Marie Pédrot2014-07-27
|
* 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
|
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
| | | If [i] or [j] is negative goals are counted from the end.
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
| | | [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
* A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵Gravatar Arnaud Spiwack2014-07-25
| | | | | or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
* 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.
* Small code sharing in TacticMatching.Gravatar Pierre-Marie Pédrot2014-07-22
|
* Correct eauto which was not dealing properly with polymorphic constants.Gravatar Matthieu Sozeau2014-07-21
|
* Redo PMP's patch to rewriting to make it purely functional using state passing.Gravatar Matthieu Sozeau2014-07-14
|
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
| | | | | Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay.
* Fix a oversight in 5bf9e67b .Gravatar Arnaud Spiwack2014-07-10
| | | | | | About 8 months after making this commit, I realised that I forgot to change a tclORELSE into a tclOR (which was the whole point of the commit to begin with). Shame on me. It does not seem to have much of an effect on efficiency, though. It may be a hair faster, but mostly indistinguishably so.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Using IStream coiterator to explicit the captured state of tactic matching ↵Gravatar Pierre-Marie Pédrot2014-07-05
| | | | results.
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
|
* More efficient implementation of Ltac match, by inlining a stream map.Gravatar Pierre-Marie Pédrot2014-07-03
|
* In setoid_rewrite, force resolution of the contraints generated by rewriting ↵Gravatar Matthieu Sozeau2014-07-02
| | | | | | | only. Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found in ATBR).
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
| | | | | message. Otherwise, a heading space was missing when calling tclFAIL from ML tactics.
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
|
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
| | | | | | elimination scheme in induction/destruct also for those names which correspond to neither the induction hypotheses nor the recursive arguments.
* Small refinement about whether it is tolerated for compatibility thatGravatar Hugo Herbelin2014-06-28
| | | | | | or-and intropatterns bind a limited number of patterns: if * or ** are used, the bound has to be used (since there is no heavy compatibility to respect for * and **). This fixes test-suite/success/intros.v.
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
| | | | | | | into a specific new cleaned file find_subterm.ml. This makes things clearer but also solves some dependencies problem between Evd, Termops and Pretype_errors.
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
| | | | | not a variable, in the future objective to factorize code between "generalize dependent" and "set", "destruct", etc.
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
| | | | proof engine. Moved it to unification.ml.
* Add an init_setoid check in rewrite to avoid trying to get undefined references.Gravatar Matthieu Sozeau2014-06-27
| | | | Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:11:54 +0000