- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.

- Test match dépendant.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 13 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 7e02d06f3..b457a55b9 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -104,7 +104,7 @@ Implicit Arguments eq_dep1 [U P].
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
-Lemma eq_sigS_eq_dep :
+Lemma eq_sigT_eq_dep :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
     existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
@@ -113,26 +113,19 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
+Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *)
+
 Lemma equiv_eqex_eqdep :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-   existS P p x = existS P q y <-> eq_dep p x q y.
+   existT P p x = existT P q y <-> eq_dep p x q y.
 Proof.
   split. 
   (* -> *)
-  apply eq_sigS_eq_dep.
+  apply eq_sigT_eq_dep.
   (* <- *)
   destruct 1; reflexivity.
 Qed.
 
-Lemma eq_sigT_eq_dep :
-  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-    existT P p x = existT P q y -> eq_dep p x q y.
-Proof.
-  intros.
-  dependent rewrite H.
-  apply eq_dep_intro.
-Qed.
-
 Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
     eq_dep p x q y -> existT P p x = existT P q y.
@@ -258,7 +251,7 @@ Section Corollaries.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
-   apply eq_sigS_eq_dep.
+   apply eq_sigT_eq_dep.
    assumption.
  Qed.