diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 10 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 5 | ||||
| -rw-r--r-- | library/nameops.ml | 5 | ||||
| -rw-r--r-- | library/nameops.mli | 2 | ||||
| -rw-r--r-- | library/universes.ml | 9 |
8 files changed, 20 insertions, 17 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 diff --git a/library/declaremods.mli b/library/declaremods.mli index c3578ec421..319d168d05 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -75,7 +75,7 @@ val register_library : Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.universe_context_set -> unit -val get_library_symbols_tbl : library_name -> Nativecode.symbol array +val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit diff --git a/library/global.ml b/library/global.ml index 49fa2ef28f..0419799b67 100644 --- a/library/global.ml +++ b/library/global.ml @@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) -let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 248e1f86dd..363bb57890 100644 --- a/library/global.mli +++ b/library/global.mli @@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit -val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) @@ -102,7 +101,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path * Nativecode.symbol array + module_path (** {6 Misc } *) diff --git a/library/library.ml b/library/library.ml index a8fbe0841c..45fce1c26c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -169,8 +169,9 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if !Flags.native_compiler then - Nativelib.link_library ~prefix ~dirname ~basename:f + (* This will not produce errors or warnings if the native compiler was + not enabled *) + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] diff --git a/library/nameops.ml b/library/nameops.ml index 02b085a7ac..3a23ab97df 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -136,6 +136,11 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous +let name_max na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + let pr_lab l = str (Label.to_string l) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nameops.mli b/library/nameops.mli index 23432ae2fa..de1f99fe0f 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit val name_cons : Name.t -> Id.t list -> Id.t list val name_app : (Id.t -> Id.t) -> Name.t -> Name.t val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - +val name_max : Name.t -> Name.t -> Name.t val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/library/universes.ml b/library/universes.ml index a3926bc6f2..1c8a5ad77d 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -723,7 +723,10 @@ let pr_constraints_map cmap = prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () ++ acc) cmap (mt ()) - + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> @@ -767,8 +770,8 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in - instantiate_with_lbound u lbound false false acc + let acc' = remove_alg l acc in + instantiate_with_lbound u lbound false false acc' else acc, (true, false, lbound) | None -> try |