From: Claudio Sacerdoti Coen Date: Mon, 29 Jan 2007 11:12:43 +0000 (+0000) Subject: Some more datatypes lifted to Type. X-Git-Tag: 0.4.95@7852~643 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2969da3e405b016a815bd22c893b1e1604226c55;p=helm.git Some more datatypes lifted to Type. --- diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma index 3be6bc9d1..6d0a68503 100644 --- a/matita/library/datatypes/constructors.ma +++ b/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 =