X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fconstructors.ma;h=6d0a68503bb809a72c689be947ef81f38e812c89;hb=4421f312e9614e608d0ddf6fa029c761f87ceb45;hp=b91a59e177f71897dbb0bba85a37214cee9c062c;hpb=7b4d519aefac94afb371a7e4da94779b40bf8608;p=helm.git

diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma
index b91a59e17..6d0a68503 100644
--- 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 =
@@ -72,4 +72,8 @@ match p with
 
 definition sndT \def \lambda A,B:Type.\lambda p: ProdT A B.
 match p with
-[(pairT a b) \Rightarrow b].
\ No newline at end of file
+[(pairT a b) \Rightarrow b].
+
+inductive option (A:Type) : Type ≝
+   None : option A
+ | Some : A → option A.
\ No newline at end of file