matitadep sould be ok, outputs warning regarding issues and

[helm.git] / matita / dama / attic / rings.ma

diff --git a/matita/dama/attic/rings.ma b/matita/dama/attic/rings.ma
index 2ea188847b81ab9c368ef18186e76831a29af8c9..d4db003dc7a57b71fe97257d7c278f060994e73d 100644 (file)
--- a/matita/dama/attic/rings.ma
+++ b/matita/dama/attic/rings.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/rings/".
+
 
 include "group.ma".
 
@@ -66,13 +66,13 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
 qed.
 
 interpretation "Ring mult" 'times a b =
- (cic:/matita/rings/mult.con _ a b).
+ (cic:/matita/attic/rings/mult.con _ a b).
 
 notation "1" with precedence 89
 for @{ 'one }.
 
 interpretation "Ring one" 'one =
- (cic:/matita/rings/one.con _).
+ (cic:/matita/attic/rings/one.con _).
 
 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
  intros;