diff options
| author | Hugo Herbelin | 2018-10-22 22:37:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-23 10:43:19 +0200 |
| commit | 62e8f2373e22a30a1ecf31efd6c7b6da5c7d5d56 (patch) | |
| tree | 5bc7d2d023f23de7f12cbeb7fc33ebe6c77af328 | |
| parent | 51caaa2b928e9a91906439f1491b78df9da27760 (diff) | |
Encapsulating declarations of primitive string syntax in a module.
| -rw-r--r-- | CHANGES.md | 5 | ||||
| -rw-r--r-- | theories/Strings/Ascii.v | 2 | ||||
| -rw-r--r-- | 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. |