From b40af3a0f07153f96fedef6092362b26fe191dfa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Oct 2000 12:28:10 +0000
Subject: Un usage en moins de l'axiome eq_rec_eq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@665 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Eqdep.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index d1f45be08e..6f19c543b9 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -46,7 +46,7 @@ Lemma eq_dep_dep1 : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y)
 Proof.
 Induction 1; Intros.
 Apply eq_dep1_intro with (refl_equal U p).
-Elim eq_rec_eq; Trivial.
+Simpl; Trivial.
 Qed.
 
 Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
-- 
cgit v1.2.3