X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=6774662a2f1aaef9ea9959f7a7b3ee7fc09ccf3c;hb=a1f4ef3daaeed7a3121a40afe55f321565669da8;hp=d529af83cd16c05d7c96495b01c12363c7e8c745;hpb=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index d529af83c..6774662a2 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -48,3 +48,4 @@ intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric;
     apply (lt0plus_orlt ????? LT0); apply mpositive;]
 qed.
     
+coercion cic:/matita/metric_space/apart_of_metric_space.con.