From 62e8f2373e22a30a1ecf31efd6c7b6da5c7d5d56 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 22 Oct 2018 22:37:00 +0200
Subject: Encapsulating declarations of primitive string syntax in a module.

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

diff --git a/CHANGES.md b/CHANGES.md
index 865e1eeb95..1f2b8067f4 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -138,8 +138,9 @@ Standard Library
 
 - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
   and `int31` are no longer available merely by `Require`ing the files
-  that define the inductives.  You must `Import` `Coq.Strings.String`,
-  `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
+  that define the inductives.  You must `Import` `Coq.Strings.String.StringSyntax`
+  (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
+  `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
   `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
   `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
   these notations.  Note that passing `-compat 8.8` or issuing
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index d1168694b2..b7c1eaa788 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -23,7 +23,7 @@ Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 Register Ascii as plugins.syntax.Ascii.
 
 Declare Scope char_scope.
-Declare ML Module "ascii_syntax_plugin".
+Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax.
 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 f6cc8c99ed..a09d518892 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -25,7 +25,7 @@ Inductive string : Set :=
   | String : ascii -> string -> string.
 
 Declare Scope string_scope.
-Declare ML Module "string_syntax_plugin".
+Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax.
 Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.
-- 
cgit v1.2.3


From c9b987029e396c9a65543b55d0ada776566c9a08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Oct 2018 10:42:00 +0200
Subject: Compat 8.8: For String/Ascii, hides "Declare ML Module" behind an
 "Export".

---
 theories/Compat/Coq88.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 950cd8242b..0aab64e4c4 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -15,11 +15,10 @@ Require Export Coq.Compat.Coq89.
     [Require].  So we make all of the relevant notations accessible in
     compatibility mode. *)
 Require Coq.Strings.Ascii Coq.Strings.String.
+Export String.StringSyntax Ascii.AsciiSyntax.
 Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
 Require Coq.Reals.Rdefinitions.
 Require Coq.Numbers.Cyclic.Int31.Int31.
-Declare ML Module "string_syntax_plugin".
-Declare ML Module "ascii_syntax_plugin".
 Declare ML Module "r_syntax_plugin".
 Declare ML Module "int31_syntax_plugin".
 Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
-- 
cgit v1.2.3