| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
subgoals and the role of the "by tac" clause swapped.
|
|
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.
|
|
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
|
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.
|
|
|
|
rather than an entire goal.
|
|
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.
|
|
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].
|
|
Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
|
|
* 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
|
|
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.
|
|
|
|
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.
|
|
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].. ].
|
|
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.
|
|
|
|
Following advice by Hugo Herbelin.
|
|
Introduced in a4043608f
|
|
- 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
|
|
|
|
|
|
catched otherwise due to the discrepancy between evars and metas.
|
|
|
|
untyped term.
|
|
|
|
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.
|
|
|
|
This allows for tail-rec calls, prevents unwanted capture of closures and
results in an overall more efficient evaluation.
|
|
|
|
potentially conflicting tactics names from different plugins.
|
|
|
|
If [i] or [j] is negative goals are counted from the end.
|
|
[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].
|
|
or local to goals.
Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
|
|
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.
|
|
|
|
|
|
|
|
backtracks, print time spent in each of successive calls.
|
|
Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
|
|
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.
|
|
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
|
|
|
|
results.
|
|
|
|
|
|
only.
Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found
in ATBR).
|
|
message. Otherwise, a heading space was missing when calling tclFAIL
from ML tactics.
|
|
|
