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