From 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 18:26:21 +0100
Subject: Merge the Linked and LinkedInteractive constructors.

There was not any difference between those after the cleanup patches that
come before.
---
 kernel/nativecode.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1b9a110379..09db29d222 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1981,9 +1981,6 @@ let register_native_file s =
 let is_code_loaded name =
   match !name with
   | NotLinked -> false
-  | LinkedInteractive s ->
-      if (is_loaded_native_file s) then true
-      else (name := NotLinked; false)
   | Linked s ->
       if is_loaded_native_file s then true
       else (name := NotLinked; false)
@@ -2192,8 +2189,7 @@ let mk_library_header (symbols : Nativevalues.symbols) =
   [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
 
 let update_location r =
-  let v = LinkedInteractive r.upd_prefix in
-  r.upd_info := v
+  r.upd_info := Linked r.upd_prefix
 
 let update_locations (ind_updates,const_updates) =
   Mindmap_env.iter (fun _ -> update_location) ind_updates;
-- 
cgit v1.2.3