models over N fixed

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

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 2266fe9e9618a08a56e5a8a91e3033e9123818a8..cda8d3fc757c711c9e6f6bda03064342b3f41d86 100644 (file)
--- 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;