X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fconcrete_spaces.ma;h=5ce337c6f831cd900544fd7be49ebbdf36ac712c;hb=6302e8ebc63beb73aa672c9c23199bdfaa3f8715;hp=ff6774be33cb8e3c8468955b489e85db69ba07c9;hpb=49045bfd9b3038ce30a1911e2345f949ed38ec8a;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
index ff6774be3..5ce337c6f 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
@@ -27,7 +27,7 @@ coercion bp'.
 definition bp'': concrete_space → objs1 BP ≝ λc.bp c.
 coercion bp''.
 
-record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
  { rp:> arrows1 ? CS1 CS2;
    respects_converges:
     ∀b,c.