6 files changed, 13 insertions, 6 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d9e32dbbf8..ce115f564f 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -19,6 +19,7 @@ Section MakeFieldPol.
 (* Field elements : R *)
 
 Variable R:Type.
+Declare Scope R_scope.
 Bind Scope R_scope with R.
 Delimit Scope R_scope with ring.
 Local Open Scope R_scope.
@@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth.
 (* Coefficients : C *)
 
 Variable C: Type.
+Declare Scope C_scope.
 Bind Scope C_scope with C.
 Delimit Scope C_scope with coef.
 
@@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N).
 
 (* Polynomial expressions : (PExpr C) *)
 
+Declare Scope PE_scope.
 Bind Scope PE_scope with PExpr.
 Delimit Scope PE_scope with poly.
 
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 523c7b02eb..1ca6227f25 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}.
   | Z0 => 0
   | Zneg p => -(gen_phiPOS p)
   end.
- Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
- Local Open Scope ZMORPHISM.
+ Declare Scope ZMORPHISM.
+ Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Open Scope ZMORPHISM.
 
  Definition get_signZ z :=
   match z with
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index a9b4d9d6f4..920b13ef49 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -12,7 +12,6 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Require Import Quote.
 Declare ML Module "newring_plugin".
 Require Export Ring_theory.
 Require Export Ring_tac.
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index e8efb362e2..26fef99bb2 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -15,7 +15,6 @@ Require Import Ring_polynom.
 Require Import BinList.
 Require Export ListTactics.
 Require Import InitialRing.
-Require Import Quote.
 Declare ML Module "newring_plugin".
 
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a736eec5e7..b05e1e85b7 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -99,7 +99,7 @@ let protect_tac_in map id =
 let rec closed_under sigma cset t =
   try
     let (gr, _) = Termops.global_of_constr sigma t in
-    Refset_env.mem gr cset
+    GlobRef.Set_env.mem gr cset
   with Not_found ->
     match EConstr.kind sigma t with
     | Cast(c,_,_) -> closed_under sigma cset c
@@ -111,7 +111,7 @@ let closed_term args _ = match args with
   let t = Option.get (Value.to_constr t) in
   let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let cs = List.fold_right Refset_env.add l Refset_env.empty in
+  let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
   if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 | _ -> assert false
 
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
new file mode 100644
index 0000000000..101246e28f
--- /dev/null
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name newring_plugin)
+ (public_name coq.plugins.setoid_ring)
+ (synopsis "Coq's setoid ring plugin")
+ (libraries coq.plugins.quote))