diff options
| author | Cyril Cohen | 2020-11-11 20:08:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-11 20:14:05 +0100 |
| commit | eb4bed01bf31c21cd13cdfbd4b81303f4f357c4e (patch) | |
| tree | 902f83d893389dfe9a4f129f325ef7d92822940f /mathcomp/ssreflect/seq.v | |
| parent | cf74596ed9f29ba4e6c125a7916f6c631366a6f3 (diff) | |
Deprecation of iota_add delayed, and not the one of iter_add
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 4 |
1 files changed, 3 insertions, 1 deletions
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 := |