Merge PR #18538: Deprecate Arith/Bool_nat

Reviewed-by: proux01 Co-authored-by: proux01 <proux01@users.noreply.github.com>
coq · Jan 25, 2024 · 2a0c713 · 2a0c713
2 parents 520a0a8 + db53867
commit 2a0c713
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 3 deletions.
diff --git a/doc/changelog/11-standard-library/18538-deprecate_Bool_nat.rst b/doc/changelog/11-standard-library/18538-deprecate_Bool_nat.rst
@@ -0,0 +1,4 @@
+- **Deprecated:**
+  The library file ``Coq.Arith.Bool_nat`` has been deprecated.
+  (`#18538 <https://github.com/coq/coq/pull/18538>`_,
+  by Pierre Rousselin).
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
@@ -103,3 +103,4 @@ theories/Numbers/NatInt/NZProperties.v
 theories/Numbers/NatInt/NZDomain.v
 theories/Numbers/Integer/Abstract/ZDivEucl.v
 theories/ZArith/Zeuclid.v
+theories/Arith/Bool_nat.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
@@ -122,7 +122,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Arith/Compare.v
     theories/Arith/EqNat.v
     theories/Arith/Euclid.v
-    theories/Arith/Bool_nat.v
     theories/Arith/Factorial.v
     theories/Arith/Wf_nat.v
     theories/Arith/Cantor.v

diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
@@ -8,32 +8,49 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+Attributes deprecated(since="8.20").
 Require Export Compare_dec.
 Require Export Peano_dec.
 Require Import Sumbool.
 
+#[local]
+Set Warnings "-deprecated".
 Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
-
 (** The decidability of equality and order relations over
     type [nat] give some boolean functions with the adequate specification. *)
-
+#[deprecated(since="8.20", note="Use Coq.Arith.Compare_dec.zerop instead")]
 Definition notzerop n := sumbool_not _ _ (zerop n).
+
+#[deprecated(since="8.20",
+note="Use Arith.Compare_dec.lt_dec and PeanoNat.Nat.nlt_ge instead")]
 Definition lt_ge_dec : forall x y, {x < y} + {x >= y} :=
   fun n m => sumbool_not _ _ (le_lt_dec m n).
 
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.ltb instead")]
 Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y).
+
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.leb instead")]
 Definition nat_ge_lt_bool x y :=
   bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)).
 
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.leb instead")]
 Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y).
+
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.ltb instead")]
 Definition nat_gt_le_bool x y :=
   bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)).
 
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.eqb instead")]
 Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y).
+
+#[deprecated(since="8.20", note="Use PeanoNat.Nat.eqb instead")]
 Definition nat_noteq_bool x y :=
   bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)).
 
+#[deprecated(since="8.20", note="Use Coq.Arith.Compare_dec.zerop instead")]
 Definition zerop_bool x := bool_of_sumbool (zerop x).
+
+#[deprecated(since="8.20", note="Use Coq.Arith.Compare_dec.zerop instead")]
 Definition notzerop_bool x := bool_of_sumbool (notzerop x).