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/environ.ml      | 1 -
 kernel/environ.mli     | 1 -
 kernel/nativecode.ml   | 6 +-----
 kernel/nativelambda.ml | 2 --
 4 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 914c951eb6..5914e66fc3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref
 
 type link_info =
   | Linked of string
-  | LinkedInteractive of string
   | NotLinked
 
 type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60696184ef..6d0ca93707 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val
 (** Linking information for the native compiler *)
 type link_info =
   | Linked of string
-  | LinkedInteractive of string
   | NotLinked
 
 type key = int CEphemeron.key option ref
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;
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index e98e97907a..18f16f427d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -111,14 +111,12 @@ let get_mind_prefix env mind =
    match !name with
    | NotLinked -> ""
    | Linked s -> s
-   | LinkedInteractive s -> s
 
 let get_const_prefix env c =
    let _,(nameref,_) = lookup_constant_key c env in
    match !nameref with
    | NotLinked -> ""
    | Linked s -> s
-   | LinkedInteractive s -> s
 
 (* A generic map function *)
 
-- 
cgit v1.2.3