diff options
Diffstat (limited to 'theories/Strings')
| -rw-r--r-- | theories/Strings/Ascii.v | 3 | ||||
| -rw-r--r-- | theories/Strings/String.v | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 79ec67b633..6a849bb0b1 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -24,6 +24,9 @@ Declare Scope char_scope. Delimit Scope char_scope with char. Bind Scope char_scope with ascii. +Register ascii as core.ascii.type. +Register Ascii as core.ascii.ascii. + Definition zero := Ascii false false false false false false false false. Definition one := Ascii true false false false false false false false. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 9d0d2f854d..b736f41a08 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -30,8 +30,9 @@ Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. -Register EmptyString as plugins.syntax.EmptyString. -Register String as plugins.syntax.String. +Register string as core.string.type. +Register EmptyString as core.string.empty. +Register String as core.string.string. (** Equality is decidable *) |