{new,setoid_}ring -> ring

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

25 files changed, 61 insertions, 61 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index b7418f54bd..56bd34f6fd 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -160,7 +160,7 @@
 /plugins/nsatz/        @coq/nsatz-maintainers
 /theories/nsatz/       @coq/nsatz-maintainers
 
-/plugins/setoid_ring/  @coq/ring-maintainers
+/plugins/ring/  @coq/ring-maintainers
 /theories/setoid_ring/ @coq/ring-maintainers
 
 /plugins/ssrmatching/  @coq/ssreflect-maintainers
diff --git a/CREDITS b/CREDITS
index 7a2d65f7c8..4f1071612d 100644
--- a/CREDITS
+++ b/CREDITS
@@ -46,7 +46,7 @@ plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/rtauto
   developed by Pierre Corbineau (LRI, 2005)
-plugins/setoid_ring
+plugins/ring
   developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
   Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
   and Bruno Barras (INRIA LogiCal, 2005-2006),
diff --git a/META.coq.in b/META.coq.in
index a6747c614b..29b3ecbcb3 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -352,19 +352,19 @@ package "plugins" (
     plugin(native)  = "zify_plugin.cmxs"
   )
 
-  package "setoid_ring" (
+  package "ring" (
 
-    description = "Coq newring plugin"
+    description = "Coq ring plugin"
     version     = "8.13"
 
     requires    = ""
-    directory   = "setoid_ring"
+    directory   = "ring"
 
-    archive(byte)    = "newring_plugin.cmo"
-    archive(native)  = "newring_plugin.cmx"
+    archive(byte)    = "ring_plugin.cmo"
+    archive(native)  = "ring_plugin.cmx"
 
-    plugin(byte)    = "newring_plugin.cmo"
-    plugin(native)  = "newring_plugin.cmxs"
+    plugin(byte)    = "ring_plugin.cmo"
+    plugin(native)  = "ring_plugin.cmxs"
   )
 
   package "extraction" (
diff --git a/Makefile.common b/Makefile.common
index 8f880e93fb..a482b9b963 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -103,7 +103,7 @@ CORESRCDIRS:=\
 
 PLUGINDIRS:=\
   omega		micromega \
-  setoid_ring 	extraction \
+  ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac		ssr             ssrsearch
@@ -140,7 +140,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
 
 OMEGACMO:=plugins/omega/omega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
-RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
+RINGCMO:=plugins/ring/ring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
 EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
 FUNINDCMO:=plugins/funind/recdef_plugin.cmo
diff --git a/Makefile.dev b/Makefile.dev
index f48a6f0d8f..5825a884c2 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -154,7 +154,7 @@ LTACVO:=$(filter theories/ltac/%, $(THEORIESVO))
 
 omega: $(OMEGAVO) $(OMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
-setoid_ring: $(RINGVO) $(RINGCMO)
+ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)
 extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
 funind: $(FUNINDCMO) $(FUNINDVO)
@@ -163,7 +163,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMO)
 btauto: $(BTAUTOVO) $(BTAUTOCMO)
 ltac: $(LTACVO) $(LTACCMO)
 
-.PHONY: omega micromega setoid_ring nsatz extraction
+.PHONY: omega micromega ring nsatz extraction
 .PHONY: funind cc rtauto btauto ltac
 
 # For emacs:
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 91cb6168e1..534f20f85b 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -30,7 +30,7 @@ exec $OCAMLDEBUG \
     -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
     -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
     -I $COQTOP/plugins/ring \
-    -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+    -I $COQTOP/plugins/rtauto \
     -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
     -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
     -I $COQTOP/ide \
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
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index ada0fc9780..3e8916673d 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -159,7 +159,7 @@ val inject : constr -> fconstr
 (** mk_atom: prevents a term from being evaluated *)
 val mk_atom : constr -> fconstr
 
-(** mk_red: makes a reducible term (used in newring) *)
+(** mk_red: makes a reducible term (used in ring) *)
 val mk_red : fterm -> fconstr
 
 val fterm_of : fconstr -> fterm
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index f3021f4ee6..c24bafc761 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -127,14 +127,14 @@ let mul = function
 
 let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
 
-let tpexpr  = gen_constant "plugins.setoid_ring.pexpr"
-let ttconst = gen_constant "plugins.setoid_ring.const"
-let ttvar = gen_constant "plugins.setoid_ring.var"
-let ttadd = gen_constant "plugins.setoid_ring.add"
-let ttsub = gen_constant "plugins.setoid_ring.sub"
-let ttmul = gen_constant "plugins.setoid_ring.mul"
-let ttopp = gen_constant "plugins.setoid_ring.opp"
-let ttpow = gen_constant "plugins.setoid_ring.pow"
+let tpexpr  = gen_constant "plugins.ring.pexpr"
+let ttconst = gen_constant "plugins.ring.const"
+let ttvar = gen_constant "plugins.ring.var"
+let ttadd = gen_constant "plugins.ring.add"
+let ttsub = gen_constant "plugins.ring.sub"
+let ttmul = gen_constant "plugins.ring.mul"
+let ttopp = gen_constant "plugins.ring.opp"
+let ttpow = gen_constant "plugins.ring.pow"
 
 let tlist = gen_constant "core.list.type"
 let lnil = gen_constant "core.list.nil"
diff --git a/plugins/ring/dune b/plugins/ring/dune
new file mode 100644
index 0000000000..080d8c672e
--- /dev/null
+++ b/plugins/ring/dune
@@ -0,0 +1,7 @@
+(library
+ (name ring_plugin)
+ (public_name coq.plugins.ring)
+ (synopsis "Coq's ring plugin")
+ (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ring))
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/ring/g_ring.mlg
index eb7710bbc2..3c800987ac 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/ring/g_ring.mlg
@@ -13,8 +13,8 @@
 open Ltac_plugin
 open Pp
 open Util
-open Newring_ast
-open Newring
+open Ring_ast
+open Ring
 open Stdarg
 open Tacarg
 open Pcoq.Constr
@@ -22,7 +22,7 @@ open Pltac
 
 }
 
-DECLARE PLUGIN "newring_plugin"
+DECLARE PLUGIN "ring_plugin"
 
 TACTIC EXTEND protect_fv
 | [ "protect_fv" string(map) "in" ident(id) ] ->
diff --git a/plugins/setoid_ring/newring.ml b/plugins/ring/ring.ml
index 5f5a974b6a..9c75175889 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/ring/ring.ml
@@ -28,7 +28,7 @@ open Libobject
 open Printer
 open Declare
 open Entries
-open Newring_ast
+open Ring_ast
 open Proofview.Notations
 
 let error msg = CErrors.user_err Pp.(str msg)
@@ -115,7 +115,7 @@ let closed_term args _ = match args with
 
 let closed_term_ast =
   let tacname = {
-    mltac_plugin = "newring_plugin";
+    mltac_plugin = "ring_plugin";
     mltac_tactic = "closed_term";
   } in
   let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
@@ -178,7 +178,7 @@ let tactic_res = ref [||]
 
 let get_res =
   let open Tacexpr in
-  let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in
+  let name = { mltac_plugin = "ring_plugin"; mltac_tactic = "get_res"; } in
   let entry = { mltac_name = name; mltac_index = 0 } in
   let tac args ist =
     let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in
@@ -212,7 +212,7 @@ let exec_tactic env evd n f args =
 let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
 let gen_reference n = lazy (Coqlib.lib_ref n)
 
-let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
+let coq_mk_Setoid = gen_constant "plugins.ring.Build_Setoid_Theory"
 let coq_None = gen_reference "core.option.None"
 let coq_Some = gen_reference "core.option.Some"
 let coq_eq = gen_constant "core.eq.type"
@@ -265,7 +265,7 @@ let znew_ring_path =
 let zltac s =
   lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
 
-let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s) [@@ocaml.warning "-3"]
+let mk_cst l s = lazy (Coqlib.coq_reference "ring" l s) [@@ocaml.warning "-3"]
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s
 
 (* Ring theory *)
diff --git a/plugins/setoid_ring/newring.mli b/plugins/ring/ring.mli
index 73d6d91434..6d24ae84d7 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/ring/ring.mli
@@ -11,7 +11,7 @@
 open Names
 open EConstr
 open Constrexpr
-open Newring_ast
+open Ring_ast
 
 val protect_tac_in : string -> Id.t -> unit Proofview.tactic
 
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/ring/ring_ast.ml
index 8b82783db9..8b82783db9 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/ring/ring_ast.ml
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/ring/ring_ast.mli
index 8b82783db9..8b82783db9 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/ring/ring_ast.mli
diff --git a/plugins/ring/ring_plugin.mlpack b/plugins/ring/ring_plugin.mlpack
new file mode 100644
index 0000000000..91d7199f9b
--- /dev/null
+++ b/plugins/ring/ring_plugin.mlpack
@@ -0,0 +1,3 @@
+Ring_ast
+Ring
+G_ring
diff --git a/plugins/setoid_ring/dune b/plugins/setoid_ring/dune
deleted file mode 100644
index 60522cd3f5..0000000000
--- a/plugins/setoid_ring/dune
+++ /dev/null
@@ -1,7 +0,0 @@
-(library
- (name newring_plugin)
- (public_name coq.plugins.setoid_ring)
- (synopsis "Coq's setoid ring plugin")
- (libraries coq.plugins.ltac))
-
-(coq.pp (modules g_newring))
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
deleted file mode 100644
index 5aa79b5868..0000000000
--- a/plugins/setoid_ring/newring_plugin.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Newring_ast
-Newring
-G_newring
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index cec1033fdf..547d180d95 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -19,7 +19,7 @@ Require Coq.ssr.ssrsetoid.
 Definition Setoid_Theory := @Equivalence.
 Definition Build_Setoid_Theory := @Build_Equivalence.
 
-Register Build_Setoid_Theory as plugins.setoid_ring.Build_Setoid_Theory.
+Register Build_Setoid_Theory as plugins.ring.Build_Setoid_Theory.
 
 Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
 Proof.
diff --git a/theories/dune b/theories/dune
index de8dcdc5b1..c2d8197ee4 100644
--- a/theories/dune
+++ b/theories/dune
@@ -23,7 +23,7 @@
    coq.plugins.btauto
    coq.plugins.rtauto
 
-   coq.plugins.setoid_ring
+   coq.plugins.ring
    coq.plugins.nsatz
    coq.plugins.omega
 
diff --git a/theories/setoid_ring/Ring_base.v b/theories/setoid_ring/Ring_base.v
index 04c7a3a83b..4986661ad1 100644
--- a/theories/setoid_ring/Ring_base.v
+++ b/theories/setoid_ring/Ring_base.v
@@ -12,7 +12,7 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Declare ML Module "newring_plugin".
+Declare ML Module "ring_plugin".
 Require Export Ring_theory.
 Require Export Ring_tac.
 Require Import InitialRing.
diff --git a/theories/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v
index e0a3d5a3bf..a13b1fc738 100644
--- a/theories/setoid_ring/Ring_polynom.v
+++ b/theories/setoid_ring/Ring_polynom.v
@@ -919,14 +919,14 @@ Section MakeRingPol.
   | PEopp : PExpr -> PExpr
   | PEpow : PExpr -> N -> PExpr.
 
- Register PExpr as plugins.setoid_ring.pexpr.
- Register PEc as plugins.setoid_ring.const.
- Register PEX as plugins.setoid_ring.var.
- Register PEadd as plugins.setoid_ring.add.
- Register PEsub as plugins.setoid_ring.sub.
- Register PEmul as plugins.setoid_ring.mul.
- Register PEopp as plugins.setoid_ring.opp.
- Register PEpow as plugins.setoid_ring.pow.
+ Register PExpr as plugins.ring.pexpr.
+ Register PEc as plugins.ring.const.
+ Register PEX as plugins.ring.var.
+ Register PEadd as plugins.ring.add.
+ Register PEsub as plugins.ring.sub.
+ Register PEmul as plugins.ring.mul.
+ Register PEopp as plugins.ring.opp.
+ Register PEpow as plugins.ring.pow.
 
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
diff --git a/theories/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v
index df54989169..76e9b1e947 100644
--- a/theories/setoid_ring/Ring_tac.v
+++ b/theories/setoid_ring/Ring_tac.v
@@ -15,7 +15,7 @@ Require Import Ring_polynom.
 Require Import BinList.
 Require Export ListTactics.
 Require Import InitialRing.
-Declare ML Module "newring_plugin".
+Declare ML Module "ring_plugin".
 
 
 (* adds a definition t' on the normal form of t and an hypothesis id