Some more datatypes lifted to Type.

diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma
index 3be6bc9d10bf1ef8592e83467d5701848f3e54c2..6d0a68503bb809a72c689be947ef81f38e812c89 100644 (file)
--- a/helm/software/matita/library/datatypes/constructors.ma
+++ b/helm/software/matita/library/datatypes/constructors.ma
@@ -19,7 +19,7 @@ inductive void : Set \def.
 
 inductive unit : Set ≝ something: unit.
 
-inductive Prod (A,B:Set) : Set \def
+inductive Prod (A,B:Type) : Type \def
 pair : A \to B \to Prod A B.
 
 interpretation "Pair construction" 'pair x y =