| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.
The following (cooked-up) example illustrates this:
Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.
Inductive tree := Node : list tree tree -> tree.
Lemma foo : tree = tree. exact eq_refl. Qed.
Fixpoint id (t : tree) :=
match t with
| Node l =>
let l := match foo in (_ = T) return list tree T with eq_refl => l end
in
match l with
| nil => Node (nil _ _)
| cons x tl => Node (cons _ _ (id x) tl)
end
end.
is accepted, but changing tree to:
Inductive tree := Node : list tree tree -> tree.
with tree2 := .
made id be rejected after the optimization.
The same problem occurred in Paco, and is now fixed.
Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
with possible further use of token "[]" + slight restructuration.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
a dependent elimination principle for Prop arguments.
|
| | |
|
| |
|
|
| |
no spacing in English before ":".
|
| |
|
|
| |
reports errors also from stderr.
|
| |
|
|
|
| |
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Since [idtac] can, now, be used even if no goal is left, this error message which assumed that the goal was still open would run at every call of the [ring] tactic. Which lead to comically many nonsensical messages on the console during Coq's compilation.
|
| |
|
|
| |
Now that [idtac] can print a single message for several goals, printing the number of goals is readable.
|
| |
|
|
| |
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.
|
| |
|
|
| |
grammar rules.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
|
| |
|
|
|
| |
When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
|
| |
|
|
|
| |
I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
|
| | |
|
| | |
|
Pierre-Marie Pédrot
Maxime Dénès
Arnaud Spiwack
Hugo Herbelin
Enrico Tassi
Pierre Boutillier
Carst Tankink