| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
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].. ].
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
The [num_goal] tactic counts the number of focused goals.
|