1 files changed, 34 insertions, 28 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 0e62e842..857ffe94 100755..100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,18 +6,48 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Logic_Type.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
-Set Implicit Arguments.
+(** This module defines type constructors for types in [Type]
+    ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
 
-(** This module defines quantification on the world [Type]
-    ([Logic.v] was defining it on the world [Set]) *)
+Set Implicit Arguments.
 
 Require Import Datatypes.
 Require Export Logic.
 
+(** Negation of a type in [Type] *)
+
 Definition notT (A:Type) := A -> False.
 
+(** Conjunction of types in [Type] *)
+
+Inductive prodT (A B:Type) : Type :=
+    pairT : A -> B -> prodT A B.
+
+Section prodT_proj.
+
+  Variables A B : Type.
+
+  Definition fstT (H:prodT A B) := match H with
+                                   | pairT x _ => x
+                                   end.
+  Definition sndT (H:prodT A B) := match H with
+                                   | pairT _ y => y
+                                   end.
+
+End prodT_proj.
+
+Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
+  (x:A) (y:B) : C := f (pairT x y).
+
+Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
+  (p:prodT A B) : C := match p with
+                       | pairT x y => f x y
+                       end.
+
+(** Properties of [identity] *)
+
 Section identity_is_a_congruence.
 
  Variables A B : Type.
@@ -62,28 +92,4 @@ Definition identity_rect_r :
  intros A x P H y H0; case sym_id with (1 := H0); trivial.
 Defined.
 
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
-
-Section prodT_proj.
-
-  Variables A B : Type.
-
-  Definition fstT (H:prodT A B) := match H with
-                                   | pairT x _ => x
-                                   end.
-  Definition sndT (H:prodT A B) := match H with
-                                   | pairT _ y => y
-                                   end.
-
-End prodT_proj.
-
-Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
-  (x:A) (y:B) : C := f (pairT x y).
-
-Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
-  (p:prodT A B) : C := match p with
-                       | pairT x y => f x y
-                       end.
-
 Hint Immediate sym_id sym_not_id: core v62.