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

2 files changed, 5 insertions, 0 deletions

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.