X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-formal_topologies.ma;h=4b667546b0179efe84950ae67e057a3c27dd3137;hb=3e4dee5271019834cfe061d43789380cb3871b7c;hp=e136821af74f5a5c025ce0923e9f39deb3116880;hpb=3d7b244a79a1c57d3355deb2f9a70764cde077b9;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
index e136821af..4b667546b 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
@@ -14,9 +14,6 @@
 
 include "o-basic_topologies.ma".
 
-definition btop_carr: BTop → Type ≝ λo:BTop. carr1 (oa_P (carrbt o)).
-coercion btop_carr.
-
 (*
 definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.