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

2 files changed, 4 insertions, 2 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 31a7fb8ad6..3f676c1888 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -13,7 +13,6 @@
     Adapted to Coq V8 by the Coq Development Team *)
 
 Require Import Bool BinPos BinNat PeanoNat Nnat.
-Declare ML Module "ascii_syntax_plugin".
 
 (** * Definition of ascii characters *)
 
@@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin".
 
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
+Declare Scope char_scope.
+Declare ML Module "ascii_syntax_plugin".
 Delimit Scope char_scope with char.
 Bind Scope char_scope with ascii.
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index be9a10c6dc..b27474ef25 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -15,7 +15,6 @@
 Require Import Arith.
 Require Import Ascii.
 Require Import Bool.
-Declare ML Module "string_syntax_plugin".
 
 (** *** Definition of strings *)
 
@@ -25,6 +24,8 @@ Inductive string : Set :=
   | EmptyString : string
   | String : ascii -> string -> string.
 
+Declare Scope string_scope.
+Declare ML Module "string_syntax_plugin".
 Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.