"Hiding" notation for implicit coercion. Cool.

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 9fd7330426ab7a70e312d43f806081ae34bd1c95..c85d1ebc1842df1e80af57928ca936766ef83f46 100644 (file)
--- a/helm/matita/library/algebra/monoids.ma
+++ b/helm/matita/library/algebra/monoids.ma
@@ -34,6 +34,12 @@ for @{ 'munit $S }.
 
 interpretation "Monoid unit" 'munit S =
  (cic:/matita/algebra/monoids/e.con S).
+ 
+notation < "M"
+for @{ 'semigroup $M }.
+
+interpretation "Semigroup coercion" 'semigroup M =
+ (cic:/matita/algebra/monoids/semigroup.con M).
 
 definition is_left_inverse ≝
  λM:Monoid.