From a14d422bcc1a44a860dd207b10d239c064d22548 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 5 Nov 2020 13:26:07 +0100 Subject: test switching Coq deprecation mechanizm --- mathcomp/ssreflect/ssrnat.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 99189f7..0aacfa4 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2030,13 +2030,14 @@ 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). + +#[deprecated(since="mathcomp 1.12.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). -- cgit v1.2.3