added support for "polymorphic" coercions

[helm.git] / matita / library / algebra / monoids.ma

diff --git a/matita/library/algebra/monoids.ma b/matita/library/algebra/monoids.ma
index c3f3cc48e8841b8139a915399030355744755038..fc6c8f956affc3a08edba8faeb6dd0f4de3ab23a 100644 (file)
--- a/matita/library/algebra/monoids.ma
+++ b/matita/library/algebra/monoids.ma
@@ -26,7 +26,7 @@ interpretation "premonoid magma coercion" 'pmmagma M =
  (cic:/matita/algebra/monoids/magma.con M).
 
 record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group: isSemiGroup M;
+ { is_semi_group:> isSemiGroup M;
    e_is_left_unit:
     is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
    e_is_right_unit: