diff options
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 76bec6f..7875323 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -2049,6 +2049,5 @@ Qed. End Solver. -Notation "@ 'limg_add'" := - (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope. -Notation limg_add := (@limg_add _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use limgD instead.")] +Notation limg_add := limgD (only parsing). |