From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 3 Jan 2009 18:30:01 +0000 (+0000)
Subject: Universe level fixed (litterally).
X-Git-Tag: make_still_working~4303
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04111561e190485400ba91eb274b2acb1b25a817;p=helm.git

Universe level fixed (litterally).
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index be985a43c..61334e540 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -15,7 +15,7 @@
 include "o-algebra.ma".
 include "o-saturations.ma".
 
-record basic_topology: Type ≝
+record basic_topology: Type2 ≝
  { carrbt:> OA;
    A: carrbt ⇒ carrbt;
    J: carrbt ⇒ carrbt;
@@ -29,7 +29,7 @@ lemma hint: OA → objs2 OA.
 qed.
 coercion hint.
 
-record continuous_relation (S,T: basic_topology) : Type ≝
+record continuous_relation (S,T: basic_topology) : Type2 ≝
  { cont_rel:> arrows2 OA S T;
    (* reduces uses eq1, saturated uses eq!!! *)
    reduced: ∀U. U = J ? U → cont_rel U = J ? (cont_rel U);