]> matita.cs.unibo.it Git - helm.git/commitdiff
Erroneously declared coercion removed
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Jan 2007 11:07:04 +0000 (11:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Jan 2007 11:07:04 +0000 (11:07 +0000)
helm/software/matita/dama/integration_algebras.ma

index 78b41cc105459b90a5709daf297f190e1596bda3..cbe629dac0ca6654fa5cca095a13317f4851ef3f 100644 (file)
@@ -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
  }.