From 174cd1c2794654c5e7f3a5687057c58489b3efd0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Jan 2007 15:48:52 +0000
Subject: Correction typo eq_rec_eq (cf bug #1339)

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

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 9055437c24..2f36b8bb59 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -303,7 +303,7 @@ Lemma eq_rect_eq :
 Proof M.eq_rect_eq U.
 
 Lemma eq_rec_eq :
-  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.
 Proof (fun p Q => M.eq_rect_eq U p Q).
 
 (** Injectivity of Dependent Equality *)
-- 
cgit v1.2.3