| Age | Commit message (Collapse) | Author |
|---|
|
- order of hypothesis was (historically) from right to left in injection but
already from left to right in decomp_eq, so no need ro fix it there
- made test Injection.v consistent with implementation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly
Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"injection" tactic when applied on an equality statement. Moreover,
hypotheses are now entered in the left-to-right order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discriminate/injection/simplify_eq acceptent maintenant un terme
comme argument. Les clauses "with" et les variantes "e" sont aussi
acceptées. Aussi, discriminate sans argument essaie maintenant
toutes les hyps quantifiées (au lieu de traiter seulement les buts
t1<>t2).
--This line, and those below, will be ignored--
M doc/refman/RefMan-tac.tex
M CHANGES
M pretyping/evd.ml
M pretyping/termops.ml
M pretyping/termops.mli
M pretyping/clenv.ml
M tactics/extratactics.ml4
M tactics/inv.ml
M tactics/equality.ml
M tactics/tactics.mli
M tactics/equality.mli
M tactics/tacticals.ml
M tactics/eqdecide.ml4
M tactics/tacinterp.ml
M tactics/tactics.ml
M tactics/extratactics.mli
M toplevel/auto_ind_decl.ml
M contrib/funind/invfun.ml
M test-suite/success/Discriminate.v
M test-suite/success/Injection.v
M proofs/clenvtac.mli
M proofs/clenvtac.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Efficacité:
- remplacement du typage par du re-typage léger
- suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?]
- remplacement des tests aveugles de projection impossible par un
test qui vérifie au fur et à mesure que les filtrages sont autorisés
Réorganisation:
- factorisation des parties communes de injEq/discrEq/decompEq
(à noter l'ordre inverse de génération des équations dans inj et decomp...)
- uniformisation des noms "e" et "ee" utilisés dans la construction des
combinateurs de discrimination
Extension:
- ajout d'une clause "as" à injection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2121 85f007b7-540e-0410-9357-904b9bb8a0f7
|
