Simplified version.

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

diff --git a/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma b/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
index 7d219b1543ac8199d040239e3e79a534ea088e86..59b5d94eeed86fd99c5b439e279b75ec947336f0 100644 (file)
--- a/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
+++ b/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
@@ -252,6 +252,14 @@ inline "cic:/CoRN/algebra/COrdFields2/R.var".
 
 (* begin hide *)
 
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
+(* NOTATION
+Notation OneR := (One:R).
+*)
+
 (* end hide *)
 
 inline "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con".