X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fattic%2Fvector_spaces.ma;h=71fe1a81be8e4cfb571654f47649ac26d91c2f67;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=5002b022c7b4be2a7288f2a0250d67fafbc1d4ea;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
index 5002b022c..71fe1a81b 100644
--- a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
@@ -30,8 +30,7 @@ record vector_space (K:field): Type \def
   vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult
 }.
 
-interpretation "Vector space external product" 'times a b =
- (cic:/matita/attic/vector_spaces/emult.con _ _ a b).
+interpretation "Vector space external product" 'times a b = (emult _ _ 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;