From 0bf91ea32d8fe2e0a6e9464950d6e7d66eadaf6b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 2 Jun 2004 15:49:21 +0000
Subject: eq2eqT et eqT2eq devenus obsolètes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5794 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Eqdep_dec.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 22476505fa..e3c3363447 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -25,7 +25,7 @@
 Set Implicit Arguments.
 
   (** Bijection between [eq] and [eqT] *)
-  Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : 
+  Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) :
     x = y :=
     match eqxy in (_ = y) return x = y with
     | refl_equal => refl_equal x
@@ -146,8 +146,7 @@ End DecidableEqDep.
      (forall x y:A, {x = y} + {x <> y}) ->
      forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
 intros.
-rewrite eq_eqT_bij.
-elim (eq2eqT p) using K_dec.
+elim p using K_dec.
 intros.
 case (H x0 y); intros.
 elim e; left; reflexivity.
@@ -155,4 +154,4 @@ elim e; left; reflexivity.
 right; red in |- *; intro neq; apply n; elim neq; reflexivity.
 
 trivial.
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3