{new,setoid_}ring -> ring

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

10 files changed, 27 insertions, 27 deletions

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