| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of
useless eta-redexes during type class instance resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
avoiding the introduction of eta-redexes. Prioritize hints over intros
in typeclass resolution to profit from that.
Add a minor fix in coqdoc by F. Garillot.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
