...

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
index 5c5fca20af2ed0d9ae0f1635cfae0d9de549e9af..76c1097198561d3ef4b16aa12ddfb5c5db44fcf8 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
@@ -22,9 +22,9 @@ record premetric_lattice_ (R : todgroup) : Type ≝ {
   join: pml_carr → pml_carr → pml_carr
 }.
 
-interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet ? ? a b).
 
-interpretation "valued lattice join" 'or a b = (join _ _ a b).
+interpretation "valued lattice join" 'or a b = (join ? ? a b).
  
 record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ {
   prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;