| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
"pat/term" for "apply term on current_hyp as pat".
|
|
an equality.
|
|
integrate to "rewrite"?) with the code of "replace".
Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
|
|
|
|
Isolating a core tactic in replace, shareable to cutrewrite.
|
|
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
|
|
- 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?
|
|
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
|
|
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
|
|
|
|
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
|
|
|
(revealed by contribution PTSF).
|
|
|
|
|
|
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
|
|
when conversion in the goal failed.
|
|
test-suite
file HoTT_coq_089.v).
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
to Ltac's value."
It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b.
The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
|
|
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.
|
|
|
|
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.
|
