{new,setoid_}ring -> ring

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

5 files changed, 12 insertions, 12 deletions

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