nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
index bf4a26643b5272cfc413c929f12325c95ed5d20c..d41a9a92234f24078e33241579d852ffcd9fb8c9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
@@ -34,15 +34,15 @@ record vlattice (R : togroup) : Type ≝ {
   meet_join_le: ∀x,y,z.  value (meet x y) ≤ value (meet x (join y z)) 
 }. 
 
-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).
  
 notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
-interpretation "lattice value" 'value2 a = (value _ _ a).
+interpretation "lattice value" 'value2 a = (value ? ? a).
 
 notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (value _ _).
+interpretation "lattice value" 'value = (value ? ?).
 
 lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. 
   μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).