fixed some regressions

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

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 010360757641cd063b04f51cc38d7b84fda32331..45e43795539a922cd6da9e661c45179f610cded9 100644 (file)
--- 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;