Erroneously declared coercion removed

diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma
index 78b41cc105459b90a5709daf297f190e1596bda3..cbe629dac0ca6654fa5cca095a13317f4851ef3f 100644 (file)
--- a/helm/software/matita/dama/integration_algebras.ma
+++ b/helm/software/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
  }.