From 31205e035316a7795ee3a1e0045148194cdcfcae Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 25 Sep 2014 09:58:03 +0200
Subject: Hurkens.v: update comments.

---
 theories/Logic/Hurkens.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 06c72a4cb0..5f1d5232fa 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -38,8 +38,11 @@
     - The [NoRetractFromTypeToProp] module proves that [Prop] cannot
       be a retract of a larger type.
 
-    - The [Prop_neq_Type] module proves that [Prop] is different from
-      any larger [Type].
+    - The [TypeNeqSmallType] module proves that [Type] is different
+      from any smaller type.
+
+    - The [PropNeqType] module proves that [Prop] is different from
+      any larger [Type]. It is an instance of the previous result.
 
     References:
 
-- 
cgit v1.2.3