freescale porting

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
index 1b775fa78659906f83967747adc838645257d2d9..857b2d1699daec9429a5aa6b100a6c1f570665c0 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
@@ -312,8 +312,7 @@ record algebra (K: field) : Type \def
    a_algebra_properties: is_algebra ? ? a_mult a_one
  }.
 
-interpretation "Algebra product" 'times a b =
- (cic:/matita/attic/integration_algebras/a_mult.con _ a b).
+interpretation "Algebra product" 'times a b = (a_mult ? a b).
 
 definition ring_of_algebra ≝
  λK.λA:algebra K.