Merge PR #18668: Deprecate NDefOps and NIso

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst

@@ -8,6 +8,6 @@
   have been deprecated.
   Users should require ``Coq.Arith.PeanoNat`` or ``Coq.Arith.NArith.BinNat``
   if they want implementations of natural numbers and
-  ``Coq.Arith.ZArith.BinInt`` if they want an implementation of integers.
+  ``Coq.Arith.ZArith.BinInt`` if they want an implementation of integers
   (`#18500 <https://github.com/coq/coq/pull/18500>`_,
   by Pierre Rousselin).

doc/changelog/11-standard-library/18501-more_NatInt_doc.rst

@@ -1,6 +1,6 @@
 - **Deprecated:**
   The library file ``Coq.Numbers.NatInt.NZProperties`` is deprecated.
   Users can require ``Coq.Numbers.NatInt.NZMulOrder`` instead and replace the
-  module ``NZProperties.NZProp`` with ``NZMulOrder.NZMulOrderProp``.
+  module ``NZProperties.NZProp`` with ``NZMulOrder.NZMulOrderProp``
   (`#18501 <https://github.com/coq/coq/pull/18501>`_,
   by Pierre Rousselin).

doc/changelog/11-standard-library/18538-deprecate_Bool_nat.rst

@@ -1,4 +1,4 @@
 - **Deprecated:**
-  The library file ``Coq.Arith.Bool_nat`` has been deprecated.
+  The library file ``Coq.Arith.Bool_nat`` has been deprecated
   (`#18538 <https://github.com/coq/coq/pull/18538>`_,
   by Pierre Rousselin).

doc/changelog/11-standard-library/18539-deprecate_NZDomain.rst

@@ -1,4 +1,4 @@
 - **Deprecated:**
-  The library file ``Coq.Numbers.NatInt.NZDomain`` is deprecated.
+  The library file ``Coq.Numbers.NatInt.NZDomain`` is deprecated
   (`#18539 <https://github.com/coq/coq/pull/18539>`_,
   by Pierre Rousselin).

doc/changelog/11-standard-library/18544-deprecate_Zeuclid.rst

@@ -1,5 +1,5 @@
 - **Deprecated:**
   The library files ``Coq.Numbers.Integers.Abstract.ZDivEucl``
-  and ``Coq.ZArith.Zeuclid`` are deprecated.
+  and ``Coq.ZArith.Zeuclid`` are deprecated
   (`#18544 <https://github.com/coq/coq/pull/18544>`_,
   by Pierre Rousselin).

doc/changelog/11-standard-library/18564-rename-push-length.rst

@@ -3,24 +3,24 @@
   became :g:`length_app`. The standard library was migrated using the following
   script:
 
-.. code-block:: sh
+  .. code-block:: sh
 
-   find theories -name '*.v' | xargs sed -i -E '
-     s/\<app_length\>/length_app/g;
-     s/\<rev_length\>/length_rev/g;
-     s/\<map_length\>/length_map/g;
-     s/\<fold_left_length\>/fold_left_S_O/g;
-     s/\<split_length_l\>/length_fst_split/g;
-     s/\<split_length_r\>/length_snd_split/g;
-     s/\<combine_length\>/length_combine/g;
-     s/\<prod_length\>/length_prod/g;
-     s/\<firstn_length\>/length_firstn/g;
-     s/\<skipn_length\>/length_skipn/g;
-     s/\<seq_length\>/length_seq/g;
-     s/\<concat_length\>/length_concat/g;
-     s/\<flat_map_length\>/length_flat_map/g;
-     s/\<list_power_length\>/length_list_power/g;
-   '
+     find theories -name '*.v' | xargs sed -i -E '
+       s/\<app_length\>/length_app/g;
+       s/\<rev_length\>/length_rev/g;
+       s/\<map_length\>/length_map/g;
+       s/\<fold_left_length\>/fold_left_S_O/g;
+       s/\<split_length_l\>/length_fst_split/g;
+       s/\<split_length_r\>/length_snd_split/g;
+       s/\<combine_length\>/length_combine/g;
+       s/\<prod_length\>/length_prod/g;
+       s/\<firstn_length\>/length_firstn/g;
+       s/\<skipn_length\>/length_skipn/g;
+       s/\<seq_length\>/length_seq/g;
+       s/\<concat_length\>/length_concat/g;
+       s/\<flat_map_length\>/length_flat_map/g;
+       s/\<list_power_length\>/length_list_power/g;
+     '
 
   (`#18564 <https://github.com/coq/coq/pull/18564>`_,
   by Andres Erbsen).

doc/changelog/11-standard-library/18668-depr_NDefOps_NIso.rst

@@ -0,0 +1,5 @@
+- **Deprecated:**
+  The library files ``Coq.Numbers.Natural.Abstract.NIso``
+  and ``Coq.Numbers.Natural.Abstract.NDefOps`` are deprecated
+  (`#18668 <https://github.com/coq/coq/pull/18668>`_,
+  by Pierre Rousselin).

doc/stdlib/hidden-files

@@ -104,3 +104,5 @@ theories/Numbers/NatInt/NZDomain.v
 theories/Numbers/Integer/Abstract/ZDivEucl.v
 theories/ZArith/Zeuclid.v
 theories/Arith/Bool_nat.v
+theories/Numbers/Natural/Abstract/NDefOps.v
+theories/Numbers/Natural/Abstract/NIso.v

doc/stdlib/index-list.html.template

@@ -282,8 +282,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/Abstract/NAddOrder.v
     theories/Numbers/Natural/Abstract/NAxioms.v
     theories/Numbers/Natural/Abstract/NBase.v
-    theories/Numbers/Natural/Abstract/NDefOps.v
-    theories/Numbers/Natural/Abstract/NIso.v
     theories/Numbers/Natural/Abstract/NMulOrder.v
     theories/Numbers/Natural/Abstract/NOrder.v
     theories/Numbers/Natural/Abstract/NStrongRec.v

theories/Numbers/Natural/Abstract/NDefOps.v

@@ -10,6 +10,8 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
+Attributes deprecated(since="8.20", note="Use PeanoNat or BinInt instead.").
+
 Require Import Bool. (* To get the orb and negb function *)
 Require Import RelationPairs.
 Require Export NStrongRec.

theories/Numbers/Natural/Abstract/NIso.v

@@ -10,6 +10,8 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
+Attributes deprecated(since="8.20", note="Please open an issue if this file is useful for you.").
+
 Require Import NBase.
 
 Module Homomorphism (N1 N2 : NAxiomsRecSig).