Merge PR #7135: Introducing an explicit `Declare Scope` command

2 files changed, 6 insertions, 2 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