aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
|
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
| | | In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
* 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
|
* Revert the change in Constrintern introduced by "Add a type of untyped term ↵Gravatar Arnaud Spiwack2014-08-06
| | | | | | | to Ltac's value." It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b. The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
| | | | | This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
* 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.
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | | | | obtained from case analysis or induction. Made it under experimental status. This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was acting at the level of logic.ml. Now acting in tactics.ml. Parts of things to be done about naming (not related to Propositions): induction on H:nat+bool produces hypotheses n and b but destruct on H produces a and b. This is because induction takes the dependent scheme whose names are statically inferred to be a and b while destruct dynamically builds a new scheme.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* Ltac's [idtac] is now interpreted outside of a goal if possible.Gravatar Arnaud Spiwack2014-08-05
| | | | It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved.
* Ltac's idtac is now implemented using the new API.Gravatar Arnaud Spiwack2014-08-05
|
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:15:04 +0000