nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / dama / dama_duality / attic / vector_spaces.ma

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 71fe1a81be8e4cfb571654f47649ac26d91c2f67..4c4602c8bf3756fe75a16520c553a8047d08c567 100644 (file)
--- 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,7 +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 = (emult _ _ 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;