| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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!
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Remove proofview_gen, which was the repository of the extracted code, and move it to proofview_monad, which has the actual interface used by the [Proofview] module to implement tactics.
|
| |
|
|
|
|
|
|
|
| |
* 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
|
| | |
|
| |
|
|
|
| |
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
|
| |
|
|
| |
- Decomment code in reductionops forgotten after debugging.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
|
| |
|
|
|
| |
explicitly or implicitly to the variables in the as and in clauses +
formatting.
|
| | |
|
| | |
|
| |
|
| |
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].. ].
|
Hugo Herbelin
Enrico Tassi
Arnaud Spiwack
Pierre Boutillier
Maxime Dénès
Pierre-Marie Pédrot
Carst Tankink
Enrico Tassi
Matthieu Sozeau