X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPolynomials.ma;h=bd621debbd884352c63447ded1d5b6a8ecf78fa8;hb=8c0ccf03dbefd83818bc3b6849634f422f8ec727;hp=033a79f4d415e91697924891eea339af4d46783d;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
index 033a79f4d..bd621debb 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
@@ -50,7 +50,7 @@ Section CPoly_CRing
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var" "CPoly_CRing__".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var".
 
 (*#*
 The intuition behind the type [cpoly] is the following
@@ -354,7 +354,7 @@ elements of the ring.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var" "CPoly_CRing_ctd__".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var".
 
 (* NOTATION
 Notation RX := (cpoly_cring CR).
@@ -364,13 +364,13 @@ Notation RX := (cpoly_cring CR).
 Section helpful_section
 *)
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var" "CPoly_CRing_ctd__helpful_section__".
+alias id "p" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var".
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var" "CPoly_CRing_ctd__helpful_section__".
+alias id "q" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var".
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var" "CPoly_CRing_ctd__helpful_section__".
+alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var".
 
-inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var" "CPoly_CRing_ctd__helpful_section__".
+alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
 
 inline "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
 
@@ -474,7 +474,7 @@ Let [R] be a ring and write [RX] for the ring of polynomials over [R].
 Section Poly_properties
 *)
 
-inline "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var" "Poly_properties__".
+alias id "R" = "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var".
 
 (* NOTATION
 Notation RX := (cpoly_cring R).
@@ -592,7 +592,7 @@ End Poly_properties
 Section Poly_Prop_Induction
 *)
 
-inline "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var" "Poly_Prop_Induction__".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var".
 
 (* NOTATION
 Notation Cpoly := (cpoly CR).