X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_Degree.ma;h=79ec88e17a1b4b6601ec283e6a853f19eb29028e;hb=02e8b3eb9d2a8a3bb3942c41b47b6ac048efd5be;hp=55a65deeb93aecaa1399415d48d8c10e11a000dd;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma index 55a65deeb..79ec88e17 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma +++ b/helm/software/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 *)