1 files changed, 34 insertions, 15 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index f71f58c6..fdd7ba35 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Datatypes.v 8872 2006-05-29 07:36:28Z herbelin $ i*)
 
 Set Implicit Arguments.
 
@@ -47,7 +47,7 @@ Inductive Empty_set : Set :=.
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [refl_identity A a] *)
 
-Inductive identity (A:Type) (a:A) : A -> Set :=
+Inductive identity (A:Type) (a:A) : A -> Type :=
     refl_identity : identity (A:=A) a a.
 Hint Resolve refl_identity: core v62.
 
@@ -57,13 +57,13 @@ Implicit Arguments identity_rect [A].
 
 (** [option A] is the extension of [A] with an extra element [None] *)
 
-Inductive option (A:Set) : Set :=
+Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
 Implicit Arguments None [A].
 
-Definition option_map (A B:Set) (f:A->B) o :=
+Definition option_map (A B:Type) (f:A->B) o :=
   match o with
   | Some a => Some (f a)
   | None => None
@@ -71,7 +71,7 @@ Definition option_map (A B:Set) (f:A->B) o :=
 
 (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
-Inductive sum (A B:Set) : Set :=
+Inductive sum (A B:Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
 
@@ -80,7 +80,7 @@ Notation "x + y" := (sum x y) : type_scope.
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 
-Inductive prod (A B:Set) : Set :=
+Inductive prod (A B:Type) : Type :=
     pair : A -> B -> prod A B.
 Add Printing Let prod.
 
@@ -88,31 +88,38 @@ Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
 Section projections.
-   Variables A B : Set.
-   Definition fst (p:A * B) := match p with
-                               | (x, y) => x
-                               end.
-   Definition snd (p:A * B) := match p with
-                               | (x, y) => y
-                               end.
+  Variables A B : Type.
+  Definition fst (p:A * B) := match p with
+                              | (x, y) => x
+                              end.
+  Definition snd (p:A * B) := match p with
+                              | (x, y) => y
+                              end.
 End projections. 
 
 Hint Resolve pair inl inr: core v62.
 
 Lemma surjective_pairing :
- forall (A B:Set) (p:A * B), p = pair (fst p) (snd p).
+ forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
 Proof.
 destruct p; reflexivity.
 Qed.
 
 Lemma injective_projections :
- forall (A B:Set) (p1 p2:A * B),
+ forall (A B:Type) (p1 p2:A * B),
    fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
 destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
 rewrite Hfst; rewrite Hsnd; reflexivity. 
 Qed.
 
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C) 
+  (x:A) (y:B) : C := f (pair x y).
+
+Definition prod_curry (A B C:Type) (f:A -> B -> C) 
+  (p:prod A B) : C := match p with
+                       | pair x y => f x y
+                       end.
 
 (** Comparison *)
 
@@ -127,3 +134,15 @@ Definition CompOpp (r:comparison) :=
   | Lt => Gt
   | Gt => Lt
   end.
+
+(* Compatibility *)
+
+Notation prodT := prod (only parsing).
+Notation pairT := pair (only parsing).
+Notation prodT_rect := prod_rect (only parsing).
+Notation prodT_rec := prod_rec (only parsing).
+Notation prodT_ind := prod_ind (only parsing).
+Notation fstT := fst (only parsing).
+Notation sndT := snd (only parsing).
+Notation prodT_uncurry := prod_uncurry (only parsing).
+Notation prodT_curry := prod_curry (only parsing).