From: Claudio Sacerdoti Coen Date: Mon, 29 Jan 2007 11:12:43 +0000 (+0000) Subject: Some more datatypes lifted to Type. X-Git-Tag: make_still_working~6502 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9962ff269442af5e37c7cefe0bb1582f5ed6af61;p=helm.git 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 3be6bc9d1..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 =