1 files 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.