Merge PR #18936: remove NArith.Ndigits, NArith.Ndist, and Strings.ByteVector

Reviewed-by: Alizter
Ack-by: proux01
Co-authored-by: Alizter <[email protected]>

Author: coqbot-app[bot]

doc/changelog/11-standard-library/18936-remove-ByteVector-Ndist-Ndigits.rst

@@ -0,0 +1,5 @@
+- **Removed:**
+  The library files ``Coq.NArith.Ndigits``, ``Coq.NArith.Ndist``, and ``Coq.Strings.ByteVector``
+  which were deprecated since 8.19
+  (`#18936 <https://github.com/coq/coq/pull/18936>`_,
+  by Andres Erbsen).

doc/stdlib/index-list.html.template

@@ -145,8 +145,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/NArith/BinNatDef.v
     theories/NArith/BinNat.v
     theories/NArith/Nnat.v
-    theories/NArith/Ndigits.v
-    theories/NArith/Ndist.v
     theories/NArith/Ndec.v
     theories/NArith/Ndiv_def.v
     theories/NArith/Ngcd_def.v
@@ -516,7 +514,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Strings/BinaryString.v
     theories/Strings/HexString.v
     theories/Strings/OctalString.v
-    theories/Strings/ByteVector.v
   </dd>
 
   <dt> <b>Reals</b>:

test-suite/bugs/bug_17466_3.v

@@ -1,4 +1,4 @@
-
+Require Coq.Strings.String.
 Require Coq.ZArith.ZArith.
 
 Axiom proof_admitted : False.

theories/NArith/NArith.v

@@ -17,7 +17,6 @@ Require Export Nnat.
 Require Export Ndiv_def.
 Require Export Nsqrt_def.
 Require Export Ngcd_def.
-Require Export Ndigits.
 Require Export NArithRing.
 
 (** [N] contains an [order] tactic for natural numbers *)

theories/NArith/Ndec.v

@@ -15,7 +15,6 @@ Require Import BinPos.
 Require Import BinNat.
 Require Import Pnat.
 Require Import Nnat.
-Require Import Ndigits.
 
 Local Open Scope N_scope.