Deprecate obsolete files in NArith

TODO: look at Ndec.v
Villetaneuse · Dec 12, 2023 · 9ddd30f · 9ddd30f
1 parent d8f2ce5
commit 9ddd30f
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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. *)