From fb4fe9ec2c00f15a745ee12357e4a8f929a4dfc0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 16:43:00 +0200
Subject: Fix minor issues

---
 compiler/ExtractBuiltin.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 65c18efd..2e46b120 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -211,15 +211,15 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "mem_replace_fwd"
-            | Lean -> "mem.replace");
+            | FStar | Coq | HOL4 -> "core_mem_replace_fwd"
+            | Lean -> "core.mem.replace");
         };
         {
           rg = rg0;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "mem_replace_back"
-            | Lean -> "mem.replace_back");
+            | FStar | Coq | HOL4 -> "core_mem_replace_back"
+            | Lean -> "core.mem.replace_back");
         };
       ] );
     ( [ "alloc"; "vec"; "Vec"; "new" ],
-- 
cgit v1.2.3