From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 5 Jan 2007 11:07:04 +0000 (+0000)
Subject: Erroneously declared coercion removed
X-Git-Tag: 0.4.95@7852~682
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18238be513728c37e46e637e73476cd98d1bddd5;p=helm.git

Erroneously declared coercion removed
---

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
  }.