From 9705ff0d0673b9c2df8fa08c8aab01d2c40bc8f6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 4 Dec 2019 13:52:39 +0100
Subject: Avoid hardcoded paths in extraction

---
 theories/Strings/Ascii.v  | 3 +++
 theories/Strings/String.v | 5 +++--
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'theories')

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 *)
 
-- 
cgit v1.2.3