matitadep sould be ok, outputs warning regarding issues and

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

diff --git a/matita/dama/attic/vector_spaces.ma b/matita/dama/attic/vector_spaces.ma
index 1e29bee24a90b1cfc6bd552b5d05182009a2a0fc..5002b022c7b4be2a7288f2a0250d67fafbc1d4ea 100644 (file)
--- a/matita/dama/attic/vector_spaces.ma
+++ b/matita/dama/attic/vector_spaces.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/vector_spaces/".
+
 
 include "attic/reals.ma".
 
@@ -31,7 +31,7 @@ record vector_space (K:field): Type \def
 }.
 
 interpretation "Vector space external product" 'times a b =
- (cic:/matita/vector_spaces/emult.con _ _ a b).
+ (cic:/matita/attic/vector_spaces/emult.con _ _ a b).
 
 record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
  { sn_positive: ∀x:V. zero R ≤ semi_norm x;