diff options
| author | Cyril Cohen | 2020-11-11 23:20:24 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-11 23:20:24 +0100 |
| commit | d0449f7e13f06ab7295f6919d1701e8adfa72d61 (patch) | |
| tree | 44ecbab31f03316130b5a763a01cb08754f00454 /mathcomp/ssreflect | |
| parent | 1890cc8cfc1725c99606b92f7a38217bd0e42bec (diff) | |
| parent | eb4bed01bf31c21cd13cdfbd4b81303f4f357c4e (diff) | |
Merge pull request #640 from CohenCyril/fix_iota_add
Deprecation of iota_add delayed, and not the one of iter_add
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index a9ddb5e..bb462a3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3748,7 +3748,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 := diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 568f8b0..0a2fbcd 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2030,15 +2030,13 @@ Notation "@ 'decr_inj_in'" := (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope. Notation decr_inj_in := (@decr_inj_in _ _) (only parsing). +Notation "@ 'iter_add'" := + (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. Notation "@ 'odd_opp'" := (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. Notation "@ 'sqrn_sub'" := (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. - -(* TODO: restore when Coq 8.10 is no longer supported *) -(* #[deprecated(since="mathcomp 1.13.0", note="Use iterD instead.")] *) -Notation iter_add := iterD (only parsing). - +Notation iter_add := (@iterD _) (only parsing). Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). |