From: Enrico Tassi Date: Fri, 5 Jan 2007 11:07:04 +0000 (+0000) Subject: Erroneously declared coercion removed X-Git-Tag: make_still_working~6541 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b58635b318fef52cca7711cdeffde2d950e75671;p=helm.git Erroneously declared coercion removed --- diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma index 78b41cc10..cbe629dac 100644 --- 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 }.