X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fintegration_algebras.ma;h=cbe629dac0ca6654fa5cca095a13317f4851ef3f;hb=a5bfa65b18a876fca982270f673c686a7d124f65;hp=78b41cc105459b90a5709daf297f190e1596bda3;hpb=810db29f760117d933ee1f74328043b8fce43847;p=helm.git

diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma
index 78b41cc10..cbe629dac 100644
--- a/matita/dama/integration_algebras.ma
+++ b/matita/dama/integration_algebras.ma
@@ -324,7 +324,7 @@ coercion cic:/matita/integration_algebras/ring_of_algebra.con.
 
 record pre_f_algebra (K:ordered_field_ch0) : Type ≝
  { fa_archimedean_riesz_space:> archimedean_riesz_space K;
-   fa_algebra_:> algebra K;
+   fa_algebra_: algebra K;
    fa_with: a_vector_space ? fa_algebra_ = rs_vector_space ? fa_archimedean_riesz_space
  }.