X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Fmonoids.ma;h=fc6c8f956affc3a08edba8faeb6dd0f4de3ab23a;hb=3cc1aec78e4c51aa766127487f19a3d38a4b56ae;hp=c3f3cc48e8841b8139a915399030355744755038;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index c3f3cc48e..fc6c8f956 100644
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/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: