X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fmetric_space.ma;h=cda8d3fc757c711c9e6f6bda03064342b3f41d86;hb=aba6841906f09875a5800f58b24862444a1f4baf;hp=2266fe9e9618a08a56e5a8a91e3033e9123818a8;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
index 2266fe9e9..cda8d3fc7 100644
--- a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
@@ -24,9 +24,9 @@ record metric_space (R: todgroup) : Type ≝ {
 }.
 
 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
-interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b).
+interpretation "metric" 'delta2 a b = (metric _ _ a b).
 notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
+interpretation "metric" 'delta = (metric _ _).
 
 lemma apart_of_metric_space: ∀R.metric_space R → apartness.
 intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;