diff options
| author | Jason Gross | 2018-11-11 09:22:51 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-11 09:22:51 -0500 |
| commit | 186d67228018a84a93de024971356249ddbde668 (patch) | |
| tree | a78cfee43c4c33cd507093148ac788190a0d061c /theories/Strings/String.v | |
| parent | ce8e37b97ce9db6f39368c50fb0ee4a7839ce754 (diff) | |
| parent | c9b987029e396c9a65543b55d0ada776566c9a08 (diff) | |
Merge PR #8795: Encapsulating declarations of primitive string syntax in a module
Diffstat (limited to 'theories/Strings/String.v')
| -rw-r--r-- | theories/Strings/String.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |