aboutsummaryrefslogtreecommitdiff
path: root/theories/Strings/Ascii.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Strings/Ascii.v')
-rw-r--r--theories/Strings/Ascii.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 3f676c1888..d1168694b2 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -20,6 +20,8 @@ Require Import Bool BinPos BinNat PeanoNat Nnat.
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
+Register Ascii as plugins.syntax.Ascii.
+
Declare Scope char_scope.
Declare ML Module "ascii_syntax_plugin".
Delimit Scope char_scope with char.