Une passe sur l'injection et la discrimination...

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

1 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index f8f7c9960..606e884ae 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -36,3 +36,29 @@ intros.
 exact (fun H => H).
 Qed.
 
+(* Test injection as *)
+
+Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z.
+intros; injection H as Hyt Hxz.
+exact Hxz.
+Qed.
+
+(* Injection does not projects at positions in Prop... allow it?
+
+Inductive t (A:Prop) : Set := c : A -> t A.
+Goal forall p q : True\/True, c _ p = c _ q -> False.
+intros.
+injection H.
+Abort.
+
+*)
+
+(* Accept does not project on discriminable positions... allow it?
+
+Goal 1=2 -> 1=0.
+intro H.
+injection H.
+intro; assumption.
+Qed.
+
+ *)