From 0aa164f8fc8adf2cd57681ef64ff598c71b5d9f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Mar 2018 15:31:19 +0200
Subject: Declaring Scope prior to loading primitive printers.

---
 theories/Strings/Ascii.v  | 3 ++-
 theories/Strings/String.v | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'theories/Strings')

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.
-- 
cgit v1.2.3