Merge the Linked and LinkedInteractive constructors.

There was not any difference between those after the cleanup patches that
come before.

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)

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

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;

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 *)