From eb4bed01bf31c21cd13cdfbd4b81303f4f357c4e Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 11 Nov 2020 20:08:21 +0100
Subject: Deprecation of iota_add delayed, and not the one of iter_add

---
 mathcomp/ssreflect/seq.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/seq.v')

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ed0b998..985c0de 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -3654,7 +3654,9 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _)
 Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing).
 Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _)
   (only parsing).
-Notation iota_add := (deprecate iota_add iotaD) (only parsing).
+(* TODO: restore when Coq 8.10 is no longer supported                *)
+(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *)
+Notation iota_add := iotaD (only parsing).
 Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing).
 
 Notation allpairs_catr :=
-- 
cgit v1.2.3