few more files, one diverges

[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 d4db003dc7a57b71fe97257d7c278f060994e73d..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,14 +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 =
- (cic:/matita/attic/rings/mult.con _ a b).
+interpretation "Ring mult" 'times a b = (mult ? a b).
 
 notation "1" with precedence 89
 for @{ 'one }.
 
-interpretation "Ring one" 'one =
- (cic:/matita/attic/rings/one.con _).
+interpretation "Ring one" 'one = (one ?).
 
 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
  intros;