diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index e246988778a29..887d853f16b67 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -19,6 +19,7 @@ Require Import Ndigits. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="TODO"). (** Obsolete results about boolean comparisons over [N], kept for compatibility with IntMap and SMC. *) diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 0b310ba9350bf..65409d4212590 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -14,6 +14,7 @@ Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat Local Open Scope N_scope. Local Open Scope program_scope. +Attributes deprecated(since="8.19", note="Use NArith.BinNat instead."). (** This file is mostly obsolete, see directly [BinNat] now. *) Local Set Warnings "-deprecated". diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 3a92395ac2360..c3cd84af6ae38 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -12,6 +12,8 @@ Require Import BinPos. Require Import BinNat. Require Import Ndigits. +Attributes deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it."). + Local Set Warnings "-deprecated". (** An ultrametric distance over [N] numbers *) diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 7614e2beffd86..81ef9fe382435 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -11,6 +11,7 @@ Require Import BinNat. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="Use NArith.BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index baac5e9d4c93e..893fb14c31cf8 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -11,6 +11,7 @@ Require Import BinPos BinNat. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="Require BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 1db7149419d5e..0054f7e63374b 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -10,6 +10,7 @@ Require Import BinNat. +Attributes deprecated(since="8.19", note="Require BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *)