diff options
| author | Cyril Cohen | 2020-11-06 11:34:40 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-06 11:34:40 +0100 |
| commit | a637acb7940706d162fe46b1359638f986d4c9bd (patch) | |
| tree | 7b30dad4e429143ae86ded4a0898b1049d4cabab /mathcomp | |
| parent | a14d422bcc1a44a860dd207b10d239c064d22548 (diff) | |
Update mathcomp/ssreflect/ssrnat.v
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 0aacfa4..568f8b0 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2035,7 +2035,8 @@ Notation "@ 'odd_opp'" := Notation "@ 'sqrn_sub'" := (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. -#[deprecated(since="mathcomp 1.12.0", note="Use iterD instead.")] +(* 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). |