X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSemiGroups.ma;h=85eac7de25a622f76c81c1da6b2391aa22fcaa0d;hb=946be00a2b9e1713e934414bd8419f267cca1077;hp=d7035869f91f7a7c9dc014035fd1f38408ae13f1;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma b/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
index d7035869f..85eac7de2 100644
--- a/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
@@ -37,7 +37,7 @@ inline "cic:/CoRN/algebra/CSemiGroups/is_CSemiGroup.con".
 
 inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup.ind".
 
-coercion "cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con 0 (* compounds *).
 
 (*#*
 %\begin{nameconvention}%
@@ -49,6 +49,10 @@ In the %{\em %names%}% of lemmas, we will denote [[+]] with [plus].
 Implicit Arguments csg_op [c].
 *)
 
+(* NOTATION
+Infix "[+]" := csg_op (at level 50, left associativity).
+*)
+
 (* End_SpecReals *)
 
 (*#* **Semigroup axioms
@@ -156,6 +160,10 @@ End Part_Function_Plus.
 Implicit Arguments Fplus [G].
 *)
 
+(* NOTATION
+Infix "{+}" := Fplus (at level 50, left associativity).
+*)
+
 (* UNEXPORTED
 Hint Resolve included_FPlus : included.
 *)