diff options
| author | Enrico Tassi | 2020-11-06 17:24:33 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-06 17:24:33 +0100 |
| commit | c33309d4279c5d6483af54b54fe6aa326e289f9b (patch) | |
| tree | 89e092d6d3ecdd2e9a89e8d9e3481b50a31846c2 | |
| parent | e1f1d3c5e778f9e427e46b9bca2e12719085a6ef (diff) | |
| parent | a637acb7940706d162fe46b1359638f986d4c9bd (diff) | |
Merge pull request #633 from CohenCyril/fix628
Delaying the deprecation of `iter_add`
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 99189f7..568f8b0 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2030,13 +2030,15 @@ 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. -Notation iter_add := (@iter_add _) (only parsing). + +(* 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 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). |