diff options
Diffstat (limited to 'theories/Strings/Ascii.v')
| -rw-r--r-- | theories/Strings/Ascii.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |