diff options
| -rw-r--r-- | kernel/environ.ml | 8 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/modops.ml | 6 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 2 | ||||
| -rw-r--r-- | kernel/nativecode.mli | 2 |
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 |