6 files changed, 16 insertions, 3 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b9935..da86f4274d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -8,6 +8,7 @@
  *************************************************************************)
 
 Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
+Declare Scope Int_scope.
 Delimit Scope Int_scope with I.
 
 (** * Abstract Integers. *)
@@ -716,6 +717,7 @@ Inductive term : Set :=
   | Topp : term -> term
   | Tvar : N -> term.
 
+Declare Scope romega_scope.
 Bind Scope romega_scope with term.
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
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/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b4144aa45e..460bdc6d23 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -86,6 +86,7 @@ Export SsrSyntax.
 (* recognize the expansion of the boolean if; using the default printer       *)
 (* avoids a spurrious trailing %GEN_IF.                                       *)
 
+Declare Scope general_if_scope.
 Delimit Scope general_if_scope with GEN_IF.
 
 Notation "'if' c 'then' v1 'else' v2" :=
@@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
 
 (* Force boolean interpretation of simple if expressions.                     *)
 
+Declare Scope boolean_if_scope.
 Delimit Scope boolean_if_scope with BOOL_IF.
 
 Notation "'if' c 'return' t 'then' v1 'else' v2" :=
@@ -125,6 +127,7 @@ Open Scope boolean_if_scope.
 (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *)
 (* Lists library) should be loaded before ssreflect so that their notations   *)
 (* do not mask all ssreflect forms.                                           *)
+Declare Scope form_scope.
 Delimit Scope form_scope with FORM.
 Open Scope form_scope.
 
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index b2d5143e36..99ff943e61 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -216,6 +216,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope fun_scope.
 Delimit Scope fun_scope with FUN.
 Open Scope fun_scope.
 
@@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y)
 Notation "@^~ x" := (fun f => f x)
   (at level 10, x at level 8, no associativity, format "@^~  x") : fun_scope.
 
+Declare Scope pair_scope.
 Delimit Scope pair_scope with PAIR.
 Open Scope pair_scope.
 
diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v
index 829ee05e11..9a53e1dd1a 100644
--- a/plugins/ssrmatching/ssrmatching.v
+++ b/plugins/ssrmatching/ssrmatching.v
@@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )"        (at level 0).
 Reserved Notation "( a 'in' b 'in' c )" (at level 0).
 Reserved Notation "( a 'as' b 'in' c )" (at level 0).
 
+Declare Scope ssrpatternscope.
+Delimit Scope ssrpatternscope with pattern.
+
 (* Notation to define shortcuts for the "X in t" part of a pattern.           *)
 Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
-Delimit Scope ssrpatternscope with pattern.
 
 (* Some shortcuts for recurrent "X in t" parts.                               *)
 Notation RHS := (X in _ = X)%pattern.