diff options
| author | Pierre-Marie Pédrot | 2020-11-09 18:26:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-12 13:59:22 +0100 |
| commit | 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 (patch) | |
| tree | 258650a01e5925b1e344662df220e7c371f6584f | |
| parent | c12471f1c5192ba1f18adac2109913c7b55ae50b (diff) | |
Merge the Linked and LinkedInteractive constructors.
There was not any difference between those after the cleanup patches that
come before.
| -rw-r--r-- | kernel/environ.ml | 1 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 6 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 2 |
4 files changed, 1 insertions, 9 deletions
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 *) |