From ff81867363f855a3ad5bba6f6bb636f20bf8a969 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jan 2006 15:58:10 +0000
Subject: [PATCH] "Hiding" notation for implicit coercion. Cool.

---
 helm/matita/library/algebra/monoids.ma | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 9fd733042..c85d1ebc1 100644
--- 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.
-- 
2.39.2