diff options
| author | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /library/declaremods.ml | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index a82f5260ba..f66656d09a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects (** For the native compiler, we cache the library values *) -type library_values = Nativecode.symbol array -let library_values = - Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" - let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = @@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv univ digest in + let mp' = Global.import cenv univ digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); - library_values := Dirmap.add dir values !library_values in let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs -let get_library_symbols_tbl dir = Dirmap.find dir !library_values +let get_library_native_symbols dir = + Safe_typing.get_library_native_symbols (Global.safe_env ()) dir let start_library dir = let mp = Global.start_library dir in |