More work on concrete spaces.

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / concrete_spaces.ma

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 ff6774be33cb8e3c8468955b489e85db69ba07c9..5ce337c6f831cd900544fd7be49ebbdf36ac712c 100644 (file)
--- 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.