From bd02346e4038871f4d4021dd84df384fc8cf9aa4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 30 Oct 2020 12:12:26 +0900
Subject: Use `exp` rather than `X` for exponents of polynomials

---
 mathcomp/algebra/poly.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'mathcomp/algebra/poly.v')

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index a95c776..e9e9c45 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -627,7 +627,7 @@ Fact polyC_multiplicative : multiplicative polyC.
 Proof. by split; first apply: polyCM. Qed.
 Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative.
 
-Lemma polyCX n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed.
+Lemma polyC_exp n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed.
 
 Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1.
 Proof.
@@ -2778,8 +2778,6 @@ Notation "@ 'polyC_muln'" :=
   (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope.
 Notation "@ 'polyC_mul'" :=
   (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_exp'" :=
-  (deprecate polyC_exp polyCX) (at level 10, only parsing) : fun_scope.
 Notation "@ 'polyC_inv'" :=
   (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope.
 Notation "@ 'lead_coef_opp'" :=
@@ -2791,7 +2789,6 @@ Notation polyC_opp := (@polyC_opp _) (only parsing).
 Notation polyC_sub := (@polyC_sub _) (only parsing).
 Notation polyC_muln := (@polyC_muln _) (only parsing).
 Notation polyC_mul := (@polyC_mul _) (only parsing).
-Notation polyC_exp := (@polyC_exp _) (only parsing).
 Notation polyC_inv := (@polyC_inv _) (only parsing).
 Notation lead_coef_opp := (@lead_coef_opp _) (only parsing).
 Notation derivn_sub := (@derivn_sub _) (only parsing).
-- 
cgit v1.2.3