X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_Degree.ma;h=79ec88e17a1b4b6601ec283e6a853f19eb29028e;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=35b49ac2c7b5abcabdc72590b07dc685b26c33e6;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
index 35b49ac2c..79ec88e17 100644
--- a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
@@ -33,13 +33,17 @@ over [R].
 *)
 
 (* UNEXPORTED
-Section Degree_def.
+Section Degree_def
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var".
 
 (* begin hide *)
 
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
 (* end hide *)
 
 (*#*
@@ -81,7 +85,7 @@ inline "cic:/CoRN/algebra/CPoly_Degree/even_cpoly.con".
 inline "cic:/CoRN/algebra/CPoly_Degree/regular.con".
 
 (* UNEXPORTED
-End Degree_def.
+End Degree_def
 *)
 
 (* UNEXPORTED
@@ -101,13 +105,17 @@ Implicit Arguments lth_of_poly [R].
 *)
 
 (* UNEXPORTED
-Section Degree_props.
+Section Degree_props
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var".
 
 (* begin hide *)
 
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
 (* end hide *)
 
 inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con".
@@ -193,7 +201,7 @@ inline "cic:/CoRN/algebra/CPoly_Degree/monic_one.con".
 inline "cic:/CoRN/algebra/CPoly_Degree/monic_apzero.con".
 
 (* UNEXPORTED
-End Degree_props.
+End Degree_props
 *)
 
 (* UNEXPORTED
@@ -205,7 +213,7 @@ Hint Resolve degree_mult_aux: algebra.
 *)
 
 (* UNEXPORTED
-Section degree_props_Field.
+Section degree_props_Field
 *)
 
 (*#* ** Degrees of polynomials over a field
@@ -214,10 +222,14 @@ polynomials over [F].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/F.var".
+alias id "F" = "cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var".
 
 (* begin hide *)
 
+(* NOTATION
+Notation FX := (cpoly_cring F).
+*)
+
 (* end hide *)
 
 inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con".
@@ -229,6 +241,6 @@ inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_mult_imp.con".
 inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult_imp.con".
 
 (* UNEXPORTED
-End degree_props_Field.
+End degree_props_Field
 *)