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 4f6fe3f86..c9e71e24a 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -137,7 +137,7 @@ Qed. which is typically not the case in coqide). *) -Open Local Scope char_scope. +Local Open Scope char_scope. Example Space := " ". Example DoubleQuote := """". |