| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Comments
--------
- The tactic specialize conveys a somehow intuitive reasoning concept
and I would support continuing maintaining it even if the design
comes in my opinion with some oddities. (Note that the experience of
MathComp and SSReflect also suggests that specialize is an
interesting concept in itself).
There are two variants to specialize:
- specialize (H args) with H an hypothesis looks natural: we
specialize H with extra arguments and the "as pattern" clause comes
naturally as an extension of it, destructuring the result using the
pattern.
- specialize term with bindings makes the choice of fully applying the
term filling missing expressions with bindings and to then behave as
generalize. Wouldn't we like a more fine-grained approach and the
result to remain in the context?
In this second case, the "as" clause works as if the term were posed
in the context with "pose proof".
|
| |
|
|
|
|
|
|
| |
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
* "f_equal" is now a tactic in ML (placed alongside congruence since
it uses it). Normally, it should be completely compatible with the
former Ltac version, except that it doesn't suffer anymore from the
"up to 5 args" earlier limitation.
* "revert" also becomes an ML tactic. This doesn't bring any real
improvement, just some more uniformity with clear and generalize.
* The experimental "narrow" tactic is removed from Tactics.v, and
replaced by an evolution of the old & undocumented "specialize"
ML tactic:
- when specialize is called on an hyp H, the specialization is
now done in place on H. For instance "specialize (H t u v)"
removes the three leading forall of H and intantiates them by
t u and v.
- otherwise specialize still works as before (i.e. as a kind of
generalize).
See the RefMan and test-suite/accept/specialize.v for more infos.
Btw, specialize can still accept an optional number for specifying
how many premises to instantiate. This number should normally
be useless now (some autodetection mecanism added). Hence this
feature is left undocumented. For the happy few still using
specialize in the old manner, beware of the slight incompatibities...
* finally, "contradict" is left as Ltac in Tactics.v, but it has
now a better shape (accepts unfolded nots and/or things in Type),
and also some documentation in the RefMan
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre Courtieu
Hugo Herbelin
letouzey
glondu