*)
(* UNEXPORTED
-Section CPoly_CRing.
+Section CPoly_CRing
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var".
(*#*
The intuition behind the type [cpoly] is the following
in terms of these generators.
*)
-inline "cic:/CoRN/algebra/CPolynomials/cpoly_zero_cs.con".
+inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__".
-inline "cic:/CoRN/algebra/CPolynomials/cpoly_linear_cs.con".
+inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__".
inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con".
inline "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con".
(* UNEXPORTED
-End CPoly_CRing.
+End CPoly_CRing
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section CPoly_CRing_ctd.
+Section CPoly_CRing_ctd
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var".
(* NOTATION
Notation RX := (cpoly_cring CR).
*)
(* UNEXPORTED
-Section helpful_section.
+Section helpful_section
*)
-inline "cic:/CoRN/algebra/CPolynomials/p.var".
+alias id "p" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var".
-inline "cic:/CoRN/algebra/CPolynomials/q.var".
+alias id "q" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var".
-inline "cic:/CoRN/algebra/CPolynomials/c.var".
+alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var".
-inline "cic:/CoRN/algebra/CPolynomials/d.var".
+alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
inline "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
inline "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con".
(* UNEXPORTED
-End helpful_section.
+End helpful_section
*)
inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con".
inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con".
(* UNEXPORTED
-End CPoly_CRing_ctd.
+End CPoly_CRing_ctd
*)
(*#*
*)
(* UNEXPORTED
-Section Poly_properties.
+Section Poly_properties
*)
-inline "cic:/CoRN/algebra/CPolynomials/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var".
(* NOTATION
Notation RX := (cpoly_cring R).
inline "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con".
(* UNEXPORTED
-End Poly_properties.
+End Poly_properties
*)
(*#* ** Induction properties of polynomials for [Prop]
*)
(* UNEXPORTED
-Section Poly_Prop_Induction.
+Section Poly_Prop_Induction
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var".
(* NOTATION
Notation Cpoly := (cpoly CR).
inline "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con".
(* UNEXPORTED
-End Poly_Prop_Induction.
+End Poly_Prop_Induction
*)
(* UNEXPORTED