Cleaner interfaces for linking locations of native compiler.

Stop sharing those references across constants of the same
module, which was triggering some bugs when using native_compute
in interactive mode in a functor declaration.

6 files changed, 12 insertions, 12 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a3a579ee0..45dfb22d3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -207,18 +207,18 @@ let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx)
 
 let lookup_constant = lookup_constant
 
-let no_link_info () = ref NotLinked
+let no_link_info = NotLinked
 
 let add_constant_key kn cb linkinfo env =
   let new_constants =
-    Cmap_env.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
+    Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
 let add_constant kn cb env =
-  add_constant_key kn cb (no_link_info ()) env
+  add_constant_key kn cb no_link_info env
 
 let constraints_of cb u =
   let univs = cb.const_universes in
@@ -366,7 +366,7 @@ let add_mind_key kn mind_key env =
   { env with env_globals = new_globals }
 
 let add_mind kn mib env =
-  let li = no_link_info () in add_mind_key kn (mib, li) env
+  let li = ref no_link_info in add_mind_key kn (mib, li) env
 
 (* Lookup of section variables *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index a20944758..91eef2898 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -127,7 +127,7 @@ val pop_rel_context : int -> env -> env
   {6 Add entries to global environment } *)
 
 val add_constant : constant -> constant_body -> env -> env
-val add_constant_key : constant -> constant_body -> Pre_env.link_info ref ->
+val add_constant_key : constant -> constant_body -> Pre_env.link_info ->
   env -> env
 
 (** Looks up in the context of global constant names 
@@ -290,4 +290,4 @@ val registered : env -> field -> bool
 val register : env -> field -> Retroknowledge.entry -> env
 
 (** Native compiler *)
-val no_link_info : unit -> Pre_env.link_info ref
+val no_link_info : Pre_env.link_info
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d91505f89..ccec3c170 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -318,7 +318,7 @@ let rec add_structure mp sign resolver linkinfo env =
 	  { mib with mind_private = Some true }
 	else mib
       in
-      Environ.add_mind_key mind (mib,linkinfo) env
+      Environ.add_mind_key mind (mib,ref linkinfo) env
     |SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
     |SFBmodtype mtb -> Environ.add_modtype mtb env
   in
@@ -337,10 +337,10 @@ let add_linked_module mb linkinfo env =
   add_module mb linkinfo env
 
 let add_structure mp sign resolver env =
-  add_structure mp sign resolver (no_link_info ()) env
+  add_structure mp sign resolver no_link_info env
 
 let add_module mb env =
-  add_module mb (no_link_info ()) env
+  add_module mb no_link_info env
 
 let add_module_type mp mtb env =
   add_module (module_body_of_type mp mtb) env
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c3f3f2d58..6a6e4282a 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -50,7 +50,7 @@ val add_module : module_body -> env -> env
 
 (** same as add_module, but for a module whose native code has been linked by
 the native compiler. The linking information is updated. *)
-val add_linked_module : module_body -> Pre_env.link_info ref -> env -> env
+val add_linked_module : module_body -> Pre_env.link_info -> env -> env
 
 (** same, for a module type *)
 val add_module_type : module_path -> module_type_body -> env -> env
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4263b3b50..2ac8e4f93 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1430,7 +1430,7 @@ let string_of_dirpath s = "N"^string_of_dirpath s
 let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)
 
 let link_info_of_dirpath dir =
-  ref (Linked (mod_uid_of_dirpath dir ^ "."))
+  Linked (mod_uid_of_dirpath dir ^ ".")
 
 let string_of_name x =
   match x with
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 7e7094963..772986521 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -67,7 +67,7 @@ val mk_library_header : dir_path -> global list
 
 val mod_uid_of_dirpath : dir_path -> string
 
-val link_info_of_dirpath : dir_path -> link_info ref
+val link_info_of_dirpath : dir_path -> link_info
 
 val update_locations : code_location_updates -> unit