From b58635b318fef52cca7711cdeffde2d950e75671 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Jan 2007 11:07:04 +0000 Subject: [PATCH] Erroneously declared coercion removed --- helm/software/matita/dama/integration_algebras.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 }. -- 2.39.2