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/String.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'theories/Strings/String.v')

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