Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 8 insertions, 15 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 94a577ca..844bff88 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
+(*i $Id: EqdepFacts.v 11095 2008-06-10 19:36:10Z herbelin $ i*)
 
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
@@ -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.
 
@@ -270,7 +263,7 @@ Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.
  
 
 (************************************************************************)
-(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
+(** * Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
 
 Module Type EqdepElimination.