X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=bd16b2bd60217b33208159b97e188c99c2b06ee3;hb=b3dd479a0a36aeea948dcea09336fe8dfec1462d;hp=595407de868cd45a7b0b89b9e35f9c0e618ed2f8;hpb=c5cee90d95a54db8897a688f0bade4c503d82e15;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index 595407de8..bd16b2bd6 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -47,7 +47,7 @@ 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.
+(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
 
 lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y.
 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.