helm_registry: added the pair unmarshaller

[helm.git] / helm / software / matita / contribs / CoRN-Decl / complex / CComplex.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
index c28c05ed188de7226c8a261799895f053b6965c4..2782cf035535572fad1c8f81f3f3fab7605e6b22 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *)
 
@@ -194,10 +194,18 @@ End Complex_Numbers.
 
 (* begin hide *)
 
+(* NOTATION
+Notation CCX := (cpoly_cring CC).
+*)
+
 (* end hide *)
 
 inline "cic:/CoRN/complex/CComplex/II.con".
 
+(* NOTATION
+Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
+*)
+
 (*#* ** Properties of [II] *)
 
 (* UNEXPORTED