carabinieri almost done

[helm.git] / helm / software / matita / dama / metric_space.ma

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index d529af83cd16c05d7c96495b01c12363c7e8c745..6774662a2f1aaef9ea9959f7a7b3ee7fc09ccf3c 100644 (file)
--- 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.