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 *)
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 *)
%\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 *)