X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fmetric_lattice.ma;h=45e43795539a922cd6da9e661c45179f610cded9;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=010360757641cd063b04f51cc38d7b84fda32331;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma
index 010360757..45e437955 100644
--- a/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma
@@ -40,9 +40,9 @@ record mlattice (R : todgroup) : Type ≝ {
 }.
 
 interpretation "Metric lattice leq" 'leq a b = 
-  (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b). 
+  (le (excess_OF_mlattice1 _ _) a b). 
 interpretation "Metric lattice geq" 'geq a b = 
-  (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b). 
+  (le (excess_OF_mlattice _ _) a b). 
 
 lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
 intros (R ml a b E); intro H; apply E; apply ml_prop1;