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/Numbers/Cyclic/Int31/Int31.v | 3 +--
 theories/Reals/Rdefinitions.v         | 7 +++++--
 theories/Strings/Ascii.v              | 3 ++-
 theories/Strings/String.v             | 3 ++-
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d91bfd4e2c..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
@@ -51,6 +49,7 @@ 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/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 857b4ec33b..932fcddaf5 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -12,12 +12,15 @@
 (**          Definitions for the axiomatization          *)
 (*********************************************************)
 
-Declare ML Module "r_syntax_plugin".
 Require Export ZArith_base.
 
 Parameter R : Set.
 
-(* Declare Scope positive_scope with Key R *)
+(* Declare primitive numeral notations for Scope R_scope *)
+Declare Scope R_scope.
+Declare ML Module "r_syntax_plugin".
+
+(* Declare Scope R_scope with Key R *)
 Delimit Scope R_scope with R.
 
 (* Automatically open scope R_scope for arguments of type R *)
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