X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_Degree.ma;h=79ec88e17a1b4b6601ec283e6a853f19eb29028e;hb=378a122bd40f832581ee3e82cc428584b6579a57;hp=55a65deeb93aecaa1399415d48d8c10e11a000dd;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
index 55a65deeb..79ec88e17 100644
--- a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
@@ -36,7 +36,7 @@ over [R].
 Section Degree_def
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var" "Degree_def__".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var".
 
 (* begin hide *)
 
@@ -108,7 +108,7 @@ Implicit Arguments lth_of_poly [R].
 Section Degree_props
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var" "Degree_props__".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var".
 
 (* begin hide *)
 
@@ -222,7 +222,7 @@ polynomials over [F].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var" "degree_props_Field__".
+alias id "F" = "cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var".
 
 (* begin hide *)