diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-31 15:48:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-31 15:48:52 +0000 |
| commit | 174cd1c2794654c5e7f3a5687057c58489b3efd0 (patch) | |
| tree | e0a3e633c319f11eba5030643ce589eb1dcb86d2 /theories/Logic/EqdepFacts.v | |
| parent | 9dd2df4c16078d41df1cf6233c9cf84fffbeee52 (diff) | |
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
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 9055437c2..2f36b8bb5 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 *) |