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

2 files changed, 6 insertions, 1 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 5a7bd9ab30..a70ecd19d8 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -46,6 +46,7 @@ Module ZEuclidProp
 
  (** We put notations in a scope, to avoid warnings about
      redefinitions of notations *)
+ Declare Scope euclid.
  Infix "/" := D.div : euclid.
  Infix "mod" := D.modulo : euclid.
  Local Open Scope euclid.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 4b2d5c13b5..995d96b314 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -13,15 +13,18 @@
 Require Import NSub ZAxioms.
 Require Export Ring.
 
+Declare Scope pair_scope.
+Local Open Scope pair_scope.
+
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-Local Open Scope pair_scope.
 
 Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
  Module Import NProp.
    Include NSubProp N.
  End NProp.
 
+Declare Scope NScope.
 Delimit Scope NScope with N.
 Bind Scope NScope with N.t.
 Infix "=="  := N.eq (at level 70) : NScope.
@@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
 
 End Z.
 
+Declare Scope ZScope.
 Delimit Scope ZScope with Z.
 Bind Scope ZScope with Z.t.
 Infix "=="  := Z.eq (at level 70) : ZScope.