X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdFields2.ma;h=655f7554d44be6b659355934fcc4b99f449ce507;hb=16d0ba4a14fd6bede3e8b3520af7deaefb4f8068;hp=3671078fa72e6346c9a61c2b4a991b217ed42209;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
index 3671078fa..655f7554d 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
+++ b/helm/software/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".