X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fdatatypes%2Fconstructors.ma;h=b91a59e177f71897dbb0bba85a37214cee9c062c;hb=b70dd6eca72985b11d7d223b8a6a84fda44cdf69;hp=3567dd915463c8b6c2f809ed8218987a67e78042;hpb=0ed7fb39e919a6a4814dc5e9d435edf924cca72f;p=helm.git

diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma
index 3567dd915..b91a59e17 100644
--- a/matita/library/datatypes/constructors.ma
+++ b/matita/library/datatypes/constructors.ma
@@ -17,6 +17,8 @@ include "logic/equality.ma".
 
 inductive void : Set \def.
 
+inductive unit : Set ≝ something: unit.
+
 inductive Prod (A,B:Set) : Set \def
 pair : A \to B \to Prod A B.