diff options
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index e7e0e35..bd39654 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -3146,9 +3146,8 @@ Canonical matrix_finAlgType (R : finComRingType) n' := Hint Resolve comm_mx_scalar comm_scalar_mx : core. -Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar) - (at level 10, only parsing) : fun_scope. -Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use comm_mx_scalar instead.")] +Notation scalar_mx_comm := comm_mx_scalar (only parsing). (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) @@ -3685,6 +3684,5 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) End mxRingOver. End mxOver. -Notation "@ 'map_mx_sub'" := - (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope. -Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use map_mxB instead.")] +Notation map_mx_sub := map_mxB (only parsing). |