X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fattic%2Fvector_spaces.ma;h=5002b022c7b4be2a7288f2a0250d67fafbc1d4ea;hb=db068aa35cc47bb881ec810bf3b904c3d7cc9379;hp=1e29bee24a90b1cfc6bd552b5d05182009a2a0fc;hpb=df666eb58afe0b312a2c4d41683d7ae4828ee8bd;p=helm.git

diff --git a/matita/dama/attic/vector_spaces.ma b/matita/dama/attic/vector_spaces.ma
index 1e29bee24..5002b022c 100644
--- 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;