Drop support for Coq 8.10 and deprecate the `deprecate` notation

- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
  the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
  have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.

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).