{new,setoid_}ring -> ring

I believe this renaming makes it easier for new contributors to discover
the code of `ring`.

3 files changed, 7 insertions, 7 deletions

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 479fa674f5..cda8a1b679 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -387,8 +387,8 @@ The syntax for adding a new ring is
       interpretation via ``Cp_phi`` (the evaluation function of power
       coefficient) is the original term, or returns ``InitialRing.NotConstant``
       if not a constant coefficient (i.e. |L_tac| is the inverse function of
-      ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
-      and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
+      ``Cp_phi``). See files ``plugins/ring/ZArithRing.v``
+      and ``plugins/ring/RealField.v`` for examples. By default the tactic
       does not recognize power expressions as ring expressions.
 
    :n:`sign @one_term`
@@ -396,7 +396,7 @@ The syntax for adding a new ring is
       outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
       term :token:`term` is a proof that a given sign function indicates expressions
       that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See
-      ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
+      ``plugins/ring/InitialRing.v`` for examples of sign function.
 
    :n:`div @one_term`
       allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with
@@ -405,7 +405,7 @@ The syntax for adding a new ring is
       euclidean division function (:n:`@one_term` has to be a proof of
       ``Ring_theory.div_theory``). For example, this function is called when
       trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
-      ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
+      ``plugins/ring/InitialRing.v`` for examples of div function.
 
    :n:`closed [ {+ @qualid } ]`
       to be documented
@@ -538,7 +538,7 @@ Dealing with fields
    The tactic must be loaded by ``Require Import Field``. New field
    structures can be declared to the system with the ``Add Field`` command
    (see below). The field of real numbers is defined in module ``RealField``
-   (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
+   (in ``plugins/ring``). It is exported by module ``Rbase``, so
    that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
    real numbers. Rational numbers in canonical form are also declared as
    a field in the module ``Qcanon``.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e276a0edcb..4b1f312105 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4726,7 +4726,7 @@ Automating
 
 .. seealso::
 
-   File plugins/setoid_ring/RealField.v for an example of instantiation,
+   File plugins/ring/RealField.v for an example of instantiation,
    theory theories/Reals for many examples of use of field.
 
 Non-logical tactics
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index ba07e6df0d..2a7b283f55 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -24,7 +24,7 @@
    (glob_files %{project_root}/plugins/nsatz/*.mlg)
    (glob_files %{project_root}/plugins/omega/*.mlg)
    (glob_files %{project_root}/plugins/rtauto/*.mlg)
-   (glob_files %{project_root}/plugins/setoid_ring/*.mlg)
+   (glob_files %{project_root}/plugins/ring/*.mlg)
    (glob_files %{project_root}/plugins/syntax/*.mlg)
    (glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
    ; Sphinx files