Simplified version.

[helm.git] / matita / contribs / CoRN-Decl / algebra / CSemiGroups.ma

diff --git a/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma b/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
index d7035869f91f7a7c9dc014035fd1f38408ae13f1..85eac7de25a622f76c81c1da6b2391aa22fcaa0d 100644 (file)
--- 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.
 *)