X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdFields2.ma;h=655f7554d44be6b659355934fcc4b99f449ce507;hb=378a122bd40f832581ee3e82cc428584b6579a57;hp=3671078fa72e6346c9a61c2b4a991b217ed42209;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma b/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma index 3671078fa..655f7554d 100644 --- a/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma +++ b/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma @@ -38,7 +38,7 @@ Section Properties_of_leEq %\end{convention}% *) -inline "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var" "Properties_of_leEq__". +alias id "R" = "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var". (* UNEXPORTED Section addition @@ -248,7 +248,7 @@ Section PosP_properties %\end{convention}% *) -inline "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var" "PosP_properties__". +alias id "R" = "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var". (* begin hide *) @@ -312,7 +312,7 @@ Implicit Arguments one_div_succ [R]. Section One_div_succ_properties *) -inline "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var" "One_div_succ_properties__". +alias id "R" = "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var". inline "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_leEq.con". @@ -344,7 +344,7 @@ Let [R] be an ordered field. %\end{convention}% *) -inline "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var" "Half_properties__". +alias id "R" = "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var". inline "cic:/CoRN/algebra/COrdFields2/half_1.con".