diff options
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index a51ec47..becacc2 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1778,6 +1778,5 @@ Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. End rpred. -Notation "@ 'polyC_mulrz'" := - (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope. -Notation polyC_mulrz := (@polyC_mulrz _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")] +Notation polyC_mulrz := polyCMz (only parsing). |