From ffe8426049f5d7d3e613b8c51c82a940994abbb4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Aug 2004 17:42:55 +0000
Subject: Ref

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6009 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/JMeq.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 6fe4dc425f..3b07322d61 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -8,7 +8,14 @@
 
 (*i $Id$ i*)
 
-(** John Major's Equality as proposed by C. Mc Bride *)
+(** John Major's Equality as proposed by Conor McBride
+
+  Reference:
+
+  [McBride] Elimination with a Motive, Proceedings of TYPES 2000,
+  LNCS 2277, pp 197-216, 2002.
+
+*)
 
 Set Implicit Arguments.
 
@@ -65,4 +72,4 @@ Lemma eq_dep_JMeq :
 Proof.
 destruct 1.
 apply JMeq_refl. 
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3