Merge branch 'v8.5'

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