nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
index 7b9eae009c353c1cc64a3b79562315b757e6a373..9d00287bc7dd1c730829921808ac0a9bdee167d8 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
@@ -65,12 +65,12 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
  apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
 qed.
 
-interpretation "Ring mult" 'times a b = (mult _ a b).
+interpretation "Ring mult" 'times a b = (mult ? a b).
 
 notation "1" with precedence 89
 for @{ 'one }.
 
-interpretation "Ring one" 'one = (one _).
+interpretation "Ring one" 'one = (one ?).
 
 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
  intros;