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

5 files changed, 14 insertions, 4 deletions

diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 3ba9d1f5ed..7b6740e94b 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -23,6 +23,7 @@ Inductive positive : Set :=
   | xO : positive -> positive
   | xH : positive.
 
+Declare Scope positive_scope.
 Delimit Scope positive_scope with positive.
 Bind Scope positive_scope with positive.
 Arguments xO _%positive.
@@ -37,6 +38,7 @@ Inductive N : Set :=
   | N0 : N
   | Npos : positive -> N.
 
+Declare Scope N_scope.
 Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Npos _%positive.
@@ -53,6 +55,7 @@ Inductive Z : Set :=
   | Zpos : positive -> Z
   | Zneg : positive -> Z.
 
+Declare Scope Z_scope.
 Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
 Arguments Zpos _%positive.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 39af62c32f..77ab624ca5 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,8 +15,6 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
-Declare ML Module "int31_syntax_plugin".
-
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
@@ -50,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31.
 Register digits as int31 bits in "coq_int31" by True.
 Register int31 as int31 type in "coq_int31" by True.
 
+Declare Scope int31_scope.
+Declare ML Module "int31_syntax_plugin".
 Delimit Scope int31_scope with int31.
 Bind Scope int31_scope with int31.
 Local Open Scope int31_scope.
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.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 3d0c005fd1..acebfcf1d2 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -220,8 +220,10 @@ End NZDomainProp.
 Module NZOfNat (Import NZ:NZDomainSig').
 
 Definition ofnat (n : nat) : t := (S^n) 0.
-Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
+
+Declare Scope ofnat.
 Local Open Scope ofnat.
+Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
 
 Lemma ofnat_zero : [O] == 0.
 Proof.