diff options
| author | Maxime Dénès | 2019-12-04 13:52:39 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-08 15:07:15 +0100 |
| commit | 9705ff0d0673b9c2df8fa08c8aab01d2c40bc8f6 (patch) | |
| tree | 2b91d0facd28b03c762812ef6bb6d19085794369 /theories/Strings | |
| parent | 8d1bd82130a39e579986a7ad6821353149fdc38f (diff) | |
Avoid hardcoded paths in extraction
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 *) |