diff options
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index c60e008d1..2b917587c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -849,7 +849,7 @@ 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 = +let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = try @@ -857,7 +857,7 @@ let register_library dir cenv (objs:library_objects) digest = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv digest in + let mp', values = 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 |