Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

18 files changed, 372 insertions, 320 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 04ee14fb..62645b23 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -21,6 +21,7 @@ open Names
 open Term
 open Declarations
 open Mod_subst
+open Globnames
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -158,93 +159,67 @@ let lookup_constant cst =
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
-let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
-  modcache := MPmap.empty;
-  let (idts,knst) = st in
-  (* Infix definition for chaining function that accumulate
-     on a and a ContextObjectSet, ContextObjectMap.  *)
-  let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
-  (* This function eases memoization, by checking if an object is already
-     stored before trying and applying a function.
-     If the object is there, the function is not fired (we are in a
-     particular case where memoized object don't need a treatment at all).
-     If the object isn't there, it is stored and the function is fired*)
-  let try_and_go o f s m =
-    if ContextObjectSet.mem o s then
-      (s,m)
-    else
-      f (ContextObjectSet.add o s) m
-  in
-  let identity2 s m = (s,m)
+(** Graph traversal of an object, collecting on the way the dependencies of
+    traversed objects *)
+let rec traverse accu t = match kind_of_term t with
+| Var id ->
+  let body () = match Global.lookup_named id with (_, body, _) -> body in
+  traverse_object accu body (VarRef id)
+| Const (kn, _) ->
+  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  traverse_object accu body (ConstRef kn)
+| Ind (ind, _) ->
+  traverse_object accu (fun () -> None) (IndRef ind)
+| Construct (cst, _) ->
+  traverse_object accu (fun () -> None) (ConstructRef cst)
+| Meta _ | Evar _ -> assert false
+| _ -> Constr.fold traverse accu t
+
+and traverse_object (curr, data) body obj =
+  let data =
+    if Refmap.mem obj data then data
+    else match body () with
+    | None -> Refmap.add obj Refset.empty data
+    | Some body ->
+      let (contents, data) = traverse (Refset.empty, data) body in
+      Refmap.add obj contents data
   in
-  (* Goes recursively into the term to see if it depends on assumptions.
-    The 3 important cases are :
-     - Const _ where we need to first unfold the constant and return
-       the needed assumptions of its body in the environment,
-     - Rel _ which means the term is a variable which has been bound
-       earlier by a Lambda or a Prod (returns [] ),
-     - Var _ which means that the term refers to a section variable or
-       a "Let" definition, in the former it is an assumption of [t],
-       in the latter is must be unfolded like a Const.
-    The other cases are straightforward recursion.
-    Calls to the environment are memoized, thus avoiding exploration of
-    the DAG of the environment as if it was a tree (can cause
-    exponential behavior and prevent the algorithm from terminating
-    in reasonable time). [s] is a set of [context_object], representing
-    the object already visited.*)
-  let rec do_constr t s acc =
-    let rec iter t =
-      match kind_of_term t with
-	| Var id -> do_memoize_id id
-	| Meta _ | Evar _ -> assert false
-	| Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) ->
-	  (iter e1)**(iter e2)
-	| LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3)
-	| App (e1, e_array) -> (iter e1)**(iter_array e_array)
-	| Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array)
-	| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
-          (iter_array e1_array) ** (iter_array e2_array)
-	| Const (kn,_) -> do_memoize_kn kn
-	| _ -> identity2 (* closed atomic types + rel *)
-    and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2
-    in iter t s acc
-
-  and add_id id s acc =
-    (* a Var can be either a variable, or a "Let" definition.*)
-    match Global.lookup_named id with
-    | (_,None,t) ->
-        (s,ContextObjectMap.add (Variable id) t acc)
-    | (_,Some bdy,_) -> do_constr bdy s acc
-
-  and do_memoize_id id =
-    try_and_go (Variable id) (add_id id)
-
-  and add_kn kn s acc =
+  (Refset.add obj curr, data)
+
+let traverse t =
+  let () = modcache := MPmap.empty in
+  traverse (Refset.empty, Refmap.empty) t
+
+(** Hopefully bullet-proof function to recover the type of a constant. It just
+    ignores all the universe stuff. There are many issues that can arise when
+    considering terms out of any valid environment, so use with caution. *)
+let type_of_constant cb = match cb.Declarations.const_type with
+| Declarations.RegularArity ty -> ty
+| Declarations.TemplateArity (ctx, arity) ->
+  Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+
+let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
+  let (idts, knst) = st in
+  (** Only keep the transitive dependencies *)
+  let (_, graph) = traverse t in
+  let fold obj _ accu = match obj with
+  | VarRef id ->
+    let (_, body, t) = Global.lookup_named id in
+    if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
+    else accu
+  | ConstRef kn ->
     let cb = lookup_constant kn in
-    let do_type cst =
-      let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in
-	(s,ContextObjectMap.add cst ctype acc)
-    in
-    let (s,acc) =
-      if Declareops.constant_has_body cb then
-        if Declareops.is_opaque cb || not (Cpred.mem kn knst) then
-          (** it is opaque *)
-          if add_opaque then do_type (Opaque kn)
-          else (s, acc)
-        else
-          if add_transparent then do_type (Transparent kn)
-          else (s, acc)
-      else (s, acc)
-    in
-      match Global.body_of_constant_body cb with
-      | None -> do_type (Axiom kn)
-      | Some body -> do_constr body s acc
-
-  and do_memoize_kn kn =
-    try_and_go (Axiom kn) (add_kn kn)
-
- in
- fun t ->
-   snd (do_constr t
-	  (ContextObjectSet.empty)
-	  (ContextObjectMap.empty))
+    if not (Declareops.constant_has_body cb) then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Axiom kn) t accu
+    else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Opaque kn) t accu
+    else if add_transparent then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Transparent kn) t accu
+    else
+      accu
+  | IndRef _ | ConstructRef _ -> accu
+  in
+  Refmap.fold fold graph ContextObjectMap.empty
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 0a2c62f5..bb36a972 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Globnames
 
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
@@ -23,8 +24,18 @@ module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : Map.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
-(** collects all the assumptions (optionally including opaque definitions)
-   on which a term relies (together with their type) *)
+(** Collects all the objects on which a term directly relies, bypassing kernel
+    opacity, together with the recursive dependence DAG of objects.
+
+    WARNING: some terms may not make sense in the environment, because they are
+    sealed inside opaque modules. Do not try to do anything fancy with those
+    terms apart from printing them, otherwise demons may fly out of your nose.
+*)
+val traverse : constr -> (Refset.t * Refset.t Refmap.t)
+
+(** Collects all the assumptions (optionally including opaque definitions)
+   on which a term relies (together with their type). The above warning of
+   {!traverse} also applies. *)
 val assumptions :
   ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr ->
     Term.types ContextObjectMap.t
diff --git a/library/declare.ml b/library/declare.ml
index 7f42a747..c3181e4c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -253,24 +253,25 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
-  let cd = (* We deal with side effects of non-opaque constants *)
+let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let cd = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry ({
-      const_entry_opaque = false; const_entry_body = bo } as de)
-    | Entries.DefinitionEntry ({
-      const_entry_polymorphic = true; const_entry_body = bo } as de)
-      ->
-        let _, seff = Future.force bo in
-        if Declareops.side_effects_is_empty seff then cd
-        else begin
-          let seff = Declareops.uniquize_side_effects seff in
-          Declareops.iter_side_effects
-            (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-          Entries.DefinitionEntry { de with
-            const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-              pt, Declareops.no_seff) }
+    | Entries.DefinitionEntry de ->
+        if export_seff ||
+           not de.const_entry_opaque ||
+           de.const_entry_polymorphic then
+          let bo = de.const_entry_body in
+          let _, seff = Future.force bo in
+          if Declareops.side_effects_is_empty seff then cd
+          else begin
+            let seff = Declareops.uniquize_side_effects seff in
+            Declareops.iter_side_effects
+              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
+            Entries.DefinitionEntry { de with
+              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
+                pt, Declareops.no_seff) }
         end
+        else cd
     | _ -> cd
   in
   let cst = {
diff --git a/library/declare.mli b/library/declare.mli
index 03b66271..d8a00db0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
diff --git a/library/global.mli b/library/global.mli
index af23d9b7..62d7ea32 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -118,9 +118,23 @@ val is_template_polymorphic : Globnames.global_reference -> bool
 
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types Univ.in_universe_context
-val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
+(** Returns the type of the constant in its global or local universe
+    context. The type should not be used without pushing it's universe
+    context in the environmnent of usage. For non-universe-polymorphic
+    constants, it does not matter. *)
 
-(** Returns the universe context of the global reference (whatever it's polymorphic status is). *)
+val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
+(** Returns the type of the constant, forgetting its universe context if
+    it is polymorphic, use with care: for polymorphic constants, the
+    type cannot be used to produce a term used by the kernel.  For safe
+    handling of polymorphic global references, one should look at a
+    particular instantiation of the reference, in some particular
+    universe context (part of an [env] or [evar_map]), see
+    e.g. [type_of_constant_in]. If you want to create a fresh instance
+    of the reference and get its type look at [Evd.fresh_global] or
+    [Evarutil.new_global] and [Retyping.get_type_of]. *)
+
+(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : Globnames.global_reference -> Univ.universe_context
 
 (** {6 Retroknowledge } *)
diff --git a/library/globnames.ml b/library/globnames.ml
index 5eb091af..3befaa9a 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Errors
 open Names
 open Term
diff --git a/library/goptions.ml b/library/goptions.ml
index 4aea3368..ef25fa59 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -268,10 +268,14 @@ let declare_option cast uncast
     begin fun v -> add_anonymous_leaf (gdecl_obj v) end
   else write,write,write
   in
+  let warn () =
+    if depr then
+      msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+  in
   let cread () = cast (read ()) in
-  let cwrite v = write (uncast v) in
-  let clwrite v = lwrite (uncast v) in
-  let cgwrite v = gwrite (uncast v) in
+  let cwrite v = warn (); write (uncast v) in
+  let clwrite v = warn (); lwrite (uncast v) in
+  let cgwrite v = warn (); gwrite (uncast v) in
   value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
   write
 
diff --git a/library/libnames.ml b/library/libnames.ml
index f2a9d041..cdaec6a3 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 =
   List.prefix_of Id.equal
     (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
 
+let is_dirpath_suffix_of dir1 dir2 =
+  let dir1 = DirPath.repr dir1 in
+  let dir2 = DirPath.repr dir2 in
+  List.prefix_of Id.equal dir1 dir2
+
 let chop_dirpath n d =
   let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
   DirPath.make (List.rev d1), DirPath.make (List.rev d2)
diff --git a/library/libnames.mli b/library/libnames.mli
index 3b5feb94..b95c0887 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t
 val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t
 val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
 
+val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool
+
 module Dirset : Set.S with type elt = DirPath.t
 module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
 
diff --git a/library/library.ml b/library/library.ml
index b078e2c4..b4261309 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -17,6 +17,59 @@ open Libobject
 open Lib
 
 (************************************************************************)
+(*s Low-level interning/externing of libraries to files *)
+
+(*s Loading from disk to cache (preparation phase) *)
+
+let (raw_extern_library, raw_intern_library) =
+  System.raw_extern_intern Coq_config.vo_magic_number
+
+(************************************************************************)
+(** Serialized objects loaded on-the-fly *)
+
+exception Faulty of string
+
+module Delayed :
+sig
+
+type 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed
+val fetch_delayed : 'a delayed -> 'a
+
+end =
+struct
+
+type 'a delayed = {
+  del_file : string;
+  del_off : int;
+  del_digest : Digest.t;
+}
+
+let in_delayed f ch =
+  let pos = pos_in ch in
+  let _, digest = System.skip_in_segment f ch in
+  { del_file = f; del_digest = digest; del_off = pos; }
+
+(** Fetching a table of opaque terms at position [pos] in file [f],
+    expecting to find first a copy of [digest]. *)
+
+let fetch_delayed del =
+  let { del_digest = digest; del_file = f; del_off = pos; } = del in
+  try
+    let ch = System.with_magic_number_check raw_intern_library f in
+    let () = seek_in ch pos in
+    let obj, _, digest' = System.marshal_in_segment f ch in
+    let () = close_in ch in
+    if not (String.equal digest digest') then raise (Faulty f);
+    obj
+  with e when Errors.noncritical e -> raise (Faulty f)
+
+end
+
+open Delayed
+
+
+(************************************************************************)
 (*s Modules on disk contain the following informations (after the magic
     number, and before the digest). *)
 
@@ -42,12 +95,19 @@ type library_t = {
   library_extra_univs : Univ.universe_context_set;
 }
 
+type library_summary = {
+  libsum_name : compilation_unit_name;
+  libsum_digests : Safe_typing.vodigest;
+  libsum_imports : compilation_unit_name array;
+}
+
 module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
-let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
+let libraries_table : library_summary LibraryMap.t ref =
+  Summary.ref LibraryMap.empty ~name:"LIBRARY"
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
@@ -89,32 +149,31 @@ let library_is_loaded dir =
   with Not_found -> false
 
 let library_is_opened dir =
-  List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list
+  List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list
 
-let loaded_libraries () =
-  List.map (fun m -> m.library_name) !libraries_loaded_list
+let loaded_libraries () = !libraries_loaded_list
 
-let opened_libraries () =
-  List.map (fun m -> m.library_name) !libraries_imports_list
+let opened_libraries () = !libraries_imports_list
 
   (* If a library is loaded several time, then the first occurrence must
      be performed first, thus the libraries_loaded_list ... *)
 
 let register_loaded_library m =
+  let libname = m.libsum_name in
   let link m =
-    let dirname = Filename.dirname (library_full_filename m.library_name) in
-    let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in
+    let dirname = Filename.dirname (library_full_filename libname) in
+    let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
     if not !Flags.no_native_compiler then
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
-    | [] -> link m; [m]
-    | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l
+    | [] -> link m; [libname]
+    | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
-  libraries_table := LibraryMap.add m.library_name m !libraries_table
+  libraries_table := LibraryMap.add libname m !libraries_table
 
   (* ... while if a library is imported/exported several time, then
      only the last occurrence is really needed - though the imported
@@ -125,7 +184,7 @@ let register_loaded_library m =
 let rec remember_last_of_each l m =
   match l with
   | [] -> [m]
-  | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m
+  | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m
   | m'::l' -> m' :: remember_last_of_each l' m
 
 let register_open_library export m =
@@ -139,17 +198,15 @@ let register_open_library export m =
 (* [open_library export explicit m] opens library [m] if not already
    opened _or_ if explicitly asked to be (re)opened *)
 
-let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name
-
 let open_library export explicit_libs m =
   if
     (* Only libraries indirectly to open are not reopen *)
     (* Libraries explicitly mentionned by the user are always reopen *)
-    List.exists (eq_lib_name m) explicit_libs
-    || not (library_is_opened m.library_name)
+    List.exists (fun m' -> DirPath.equal m m') explicit_libs
+    || not (library_is_opened m)
   then begin
     register_open_library export m;
-    Declaremods.really_import_module (MPfile m.library_name)
+    Declaremods.really_import_module (MPfile m)
   end
   else
     if export then
@@ -164,47 +221,44 @@ let open_libraries export modl =
       (fun l m ->
          let subimport =
            Array.fold_left
-             (fun l m -> remember_last_of_each l (try_find_library m))
-             l m.library_imports
-         in remember_last_of_each subimport m)
+             (fun l m -> remember_last_of_each l m)
+             l m.libsum_imports
+         in remember_last_of_each subimport m.libsum_name)
       [] modl in
-  List.iter (open_library export modl) to_open_list
+  let explicit = List.map (fun m -> m.libsum_name) modl in
+  List.iter (open_library export explicit) to_open_list
 
 
 (**********************************************************************)
-(* import and export  -  synchronous operations*)
+(* import and export of libraries - synchronous operations            *)
+(* at the end similar to import and export of modules except that it  *)
+(* is optimized: when importing several libraries at the same time    *)
+(* which themselves indirectly imports the very same modules, these   *)
+(* ones are imported only ones *)
 
-let open_import i (_,(dir,export)) =
+let open_import_library i (_,(modl,export)) =
   if Int.equal i 1 then
     (* even if the library is already imported, we re-import it *)
     (* if not (library_is_opened dir) then *)
-      open_libraries export [try_find_library dir]
+      open_libraries export (List.map try_find_library modl)
 
-let cache_import obj =
-  open_import 1 obj
+let cache_import_library obj =
+  open_import_library 1 obj
 
-let subst_import (_,o) = o
+let subst_import_library (_,o) = o
 
-let classify_import (_,export as obj) =
+let classify_import_library (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let in_import : DirPath.t * bool -> obj =
+let in_import_library : DirPath.t list * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
-       cache_function = cache_import;
-       open_function = open_import;
-       subst_function = subst_import;
-       classify_function = classify_import }
+       cache_function = cache_import_library;
+       open_function = open_import_library;
+       subst_function = subst_import_library;
+       classify_function = classify_import_library }
 
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
-
-(*s Loading from disk to cache (preparation phase) *)
-
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
-
-(************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
 exception LibUnmappedDir
@@ -214,8 +268,9 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = Loadpath.expand_root_path pref in
+  let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
+  let loadpath = List.map fst loadpath in
   let find ext =
     try
       let name = Id.to_string base ^ ext in
@@ -232,10 +287,20 @@ let locate_absolute_library dir =
   | [vo;vi] -> dir, vo
   | _ -> assert false
 
-let locate_qualified_library warn qid =
+let locate_qualified_library ?root ?(warn = true) qid =
   (* Search library in loadpath *)
   let dir, base = repr_qualid qid in
-  let loadpath = Loadpath.expand_path dir in
+  let loadpath = match root with
+  | None -> Loadpath.expand_path dir
+  | Some root ->
+    let filter path =
+      if is_dirpath_prefix_of root path then
+        let path = drop_dirpath_prefix root path in
+        is_dirpath_suffix_of dir path
+      else false
+    in
+    Loadpath.filter_path filter
+  in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   let find ext =
     try
@@ -279,14 +344,6 @@ let try_locate_absolute_library dir =
     | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir)
     | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir)
 
-let try_locate_qualified_library (loc,qid) =
-  try
-    let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
-    dir,f
-  with
-    | LibUnmappedDir -> error_unmapped_dir qid
-    | LibNotFound -> error_lib_not_found qid
-
 (************************************************************************)
 (** {6 Tables of opaque proof terms} *)
 
@@ -296,34 +353,10 @@ let try_locate_qualified_library (loc,qid) =
     terms, and access them only when a specific command (e.g. Print or
     Print Assumptions) needs it. *)
 
-exception Faulty
-
-(** Fetching a table of opaque terms at position [pos] in file [f],
-    expecting to find first a copy of [digest]. *)
-
-let fetch_table what dp (f,pos,digest) =
-  let dir_path = Names.DirPath.to_string dp in
-  try
-    msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
-    let ch = System.with_magic_number_check raw_intern_library f in
-    let () = seek_in ch pos in
-    if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
-    let table, pos', digest' = System.marshal_in_segment f ch in
-    let () = close_in ch in
-    let ch' = open_in f in
-    if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty;
-    let () = close_in ch' in
-    table
-  with e when Errors.noncritical e ->
-    error
-      ("The file "^f^" (bound to " ^ dir_path ^
-      ") is inaccessible or corrupted,\n" ^
-      "cannot load some "^what^" in it.\n")
-
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of string * int * Digest.t
+  | ToFetch of 'a Future.computation array delayed
   | Fetched of 'a Future.computation array
 
 let opaque_tables =
@@ -336,25 +369,33 @@ let add_opaque_table dp st =
 let add_univ_table dp st =
   univ_tables := LibraryMap.add dp st !univ_tables
 
-let access_table fetch_table add_table tables dp i =
-  let t = match LibraryMap.find dp tables with
+let access_table what tables dp i =
+  let t = match LibraryMap.find dp !tables with
     | Fetched t -> t
-    | ToFetch (f,pos,digest) ->
-      let t = fetch_table dp (f,pos,digest) in
-      add_table dp (Fetched t);
+    | ToFetch f ->
+      let dir_path = Names.DirPath.to_string dp in
+      msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      let t =
+        try fetch_delayed f
+        with Faulty f ->
+          error
+            ("The file "^f^" (bound to " ^ dir_path ^
+            ") is inaccessible or corrupted,\n" ^
+            "cannot load some "^what^" in it.\n")
+      in
+      tables := LibraryMap.add dp (Fetched t) !tables;
       t
   in
   assert (i < Array.length t); t.(i)
 
 let access_opaque_table dp i =
-  access_table
-    (fetch_table "opaque proofs")
-    add_opaque_table !opaque_tables dp i
+  let what = "opaque proofs" in
+  access_table what opaque_tables dp i
+
 let access_univ_table dp i =
   try
-    Some (access_table 
-            (fetch_table "universe contexts of opaque proofs")
-            add_univ_table !univ_tables dp i)
+    let what = "universe contexts of opaque proofs" in
+    Some (access_table what univ_tables dp i)
   with Not_found -> None
 
 let () =
@@ -381,15 +422,22 @@ let mk_library md digests univs =
     library_extra_univs = univs;
   }
 
+let mk_summary m = {
+  libsum_name = m.library_name;
+  libsum_imports = m.library_imports;
+  libsum_digests = m.library_digests;
+}
+
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
   let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let pos, digest = System.skip_in_segment f ch in
+  let _ = System.skip_in_segment f ch in
+  let (del_opaque : seg_proofs delayed) = in_delayed f ch in
   close_in ch;
   register_library_filename lmd.md_name f;
-  add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
+  add_opaque_table lmd.md_name (ToFetch del_opaque);
   let open Safe_typing in
   match univs with
   | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
@@ -402,16 +450,13 @@ let intern_from_file f =
 
 module DPMap = Map.Make(DirPath)
 
-let deps_to_string deps =
-  Array.fold_left (fun s (n, _) -> s^"\n  - "^(DirPath.to_string n)) "" deps
-
 let rec intern_library (needed, contents) (dir, f) from =
   Pp.feedback(Feedback.FileDependency (from, f));
   (* Look if in the current logical environment *)
-  try find_library dir, (needed, contents)
+  try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
-  try DPMap.find dir contents, (needed, contents)
+  try (DPMap.find dir contents).library_digests, (needed, contents)
   with Not_found ->
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
   let m = intern_from_file f in
@@ -421,15 +466,15 @@ let rec intern_library (needed, contents) (dir, f) from =
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
-  m, intern_library_deps (needed, contents) dir m (Some f)
+  m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
 
 and intern_library_deps libs dir m from =
   let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
 and intern_mandatory_library caller from libs (dir,d) =
-  let m, libs = intern_library libs (try_locate_absolute_library dir) from in
-  if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then
+  let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
+  if not (Safe_typing.digest_match ~actual:digest ~required:d) then
     errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
       ".vo makes inconsistent assumptions over library " ^
       DirPath.to_string dir));
@@ -500,7 +545,7 @@ let register_library m =
     m.library_objects
     m.library_digests
     m.library_extra_univs;
-  register_loaded_library m
+  register_loaded_library (mk_summary m)
 
 (* Follow the semantics of Anticipate object:
    - called at module or module type closing when a Require occurs in
@@ -543,23 +588,19 @@ let require_library_from_dirpath modrefl export =
       begin
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
-	  List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+	  add_anonymous_leaf (in_import_library (modrefl,exp)))
 	  export
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library qidl export =
-  let modrefl = List.map try_locate_qualified_library qidl in
-    require_library_from_dirpath modrefl export
-
 let require_library_from_file idopt file export =
   let modref,needed = rec_intern_library_from_file idopt file in
   let needed = List.rev_map snd needed in
   if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+    Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp)))
       export
   end
   else
@@ -568,21 +609,38 @@ let require_library_from_file idopt file export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let import_module export (loc,qid) =
-  try
-    match Nametab.locate_module qid with
-      | MPfile dir ->
-	  if Lib.is_module_or_modtype () || not export then
-	    add_anonymous_leaf (in_import (dir, export))
-	  else
-	    add_anonymous_leaf (in_import (dir, export))
-      | mp ->
-	  Declaremods.import_module export mp
-  with
-      Not_found ->
-	user_err_loc
-          (loc,"import_library",
-	  str ((string_of_qualid qid)^" is not a module"))
+let safe_locate_module (loc,qid) =
+  try Nametab.locate_module qid
+  with Not_found ->
+    user_err_loc
+      (loc,"import_library", str (string_of_qualid qid ^ " is not a module"))
+
+let import_module export modl =
+  (* Optimization: libraries in a raw in the list are imported
+     "globally".  If there is non-library in the list; it breaks the
+     optimization For instance: "Import Arith MyModule Zarith" will
+     not be optimized (possibly resulting in redefinitions, but
+     "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule"
+     will have the submodules imported by both Arith and ZArith
+     imported only once *)
+  let flush = function
+    | [] -> ()
+    | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
+  let rec aux acc = function
+    | (loc,dir as m) :: l ->
+        let m,acc =
+          try Nametab.locate_module dir, acc
+          with Not_found-> flush acc; safe_locate_module m, [] in
+        (match m with
+        | MPfile dir -> aux (dir::acc) l
+        | mp ->
+            flush acc;
+            try Declaremods.import_module export mp; aux [] l
+            with Not_found ->
+              user_err_loc (loc,"import_library",
+                str ((string_of_qualid dir)^" is not a module")))
+    | [] -> flush acc
+  in aux [] modl
 
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
@@ -654,10 +712,13 @@ let load_library_todo f =
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
 
 let current_deps () =
-  List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list
+  let map name =
+    let m = try_find_library name in
+    (name, m.libsum_digests)
+  in
+  List.map map !libraries_loaded_list
 
-let current_reexports () =
-  List.map (fun m -> m.library_name) !libraries_exports_list
+let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
   errorlabstrm ""
@@ -683,7 +744,7 @@ let save_library_to ?todo dir f otab =
         f ^ "o", Future.UUIDSet.empty
     | Some (l,_) ->
         f ^ "io",
-        List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e)
+        List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~except dir in
   let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
@@ -692,14 +753,17 @@ let save_library_to ?todo dir f otab =
     | None -> None, None, None
     | Some (tasks, rcbackup) ->
         let tasks =
-          List.map Stateid.(fun r ->
-            { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in
+          List.map Stateid.(fun (r,b) ->
+            try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
+            with Not_found -> assert b; { r with uuid = -1 }, b)
+          tasks in
         Some (tasks,rcbackup),
         Some (univ_table,Univ.ContextSet.empty,false),
         Some disch_table in
   let except =
     Future.UUIDSet.fold (fun uuid acc ->
-      Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc)
+      try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
+      with Not_found -> acc)
       except Int.Set.empty in
   let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
   Array.iteri (fun i x ->
@@ -750,11 +814,7 @@ let save_library_raw f lib univs proofs =
 
 open Printf
 
-let mem s =
-  let m = try_find_library s in
-  h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
-		 (CObj.size_kb m) (CObj.size_kb m.library_compiled)
-		 (CObj.size_kb m.library_objects)))
+let mem s = Pp.mt ()
 
 module StringOrd = struct type t = string let compare = String.compare end
 module StringSet = Set.Make(StringOrd)
@@ -762,7 +822,7 @@ module StringSet = Set.Make(StringOrd)
 let get_used_load_paths () =
   StringSet.elements
     (List.fold_left (fun acc m -> StringSet.add
-      (Filename.dirname (library_full_filename m.library_name)) acc)
+      (Filename.dirname (library_full_filename m)) acc)
        StringSet.empty !libraries_loaded_list)
 
 let _ = Nativelib.get_load_paths := get_used_load_paths
diff --git a/library/library.mli b/library/library.mli
index 13d83a5c..35067068 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -21,7 +21,6 @@ open Libnames
 (** {6 ... } *)
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
-val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
 val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
@@ -37,14 +36,14 @@ type seg_proofs = Term.constr Future.computation array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
-val import_module : bool -> qualid located -> unit
+val import_module : bool -> qualid located list -> unit
 
 (** {6 Start the compilation of a library } *)
 val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
 val save_library_to :
-  ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) ->
+  ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
@@ -73,8 +72,14 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  bool -> qualid -> library_location * DirPath.t * CUnix.physical_path
-val try_locate_qualified_library : qualid located -> DirPath.t * string
+  ?root:DirPath.t -> ?warn:bool -> qualid ->
+  library_location * DirPath.t * CUnix.physical_path
+(** Locates a library by implicit name.
+
+  @raise LibUnmappedDir if the library is not in the path
+  @raise LibNotFound if there is no corresponding file in the path
+
+*)
 
 (** {6 Statistics: display the memory use of a library. } *)
 val mem : DirPath.t -> Pp.std_ppcmds
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 5876eedd..26af809e 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -12,14 +12,12 @@ open Errors
 open Names
 open Libnames
 
-type path_type = ImplicitPath | ImplicitRootPath | RootPath
-
 (** Load paths. Mapping from physical to logical paths. *)
 
 type t = {
   path_physical : CUnix.physical_path;
   path_logical : DirPath.t;
-  path_type : path_type;
+  path_implicit : bool;
 }
 
 let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
@@ -54,32 +52,35 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
-let add_load_path phys_path path_type coq_path =
+let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
   let binding = {
     path_logical = coq_path;
     path_physical = phys_path;
-    path_type = path_type;
+    path_implicit = implicit;
   } in
   match List.filter filter !load_paths with
   | [] ->
     load_paths := binding :: !load_paths
-  | [p] ->
-    let dir = p.path_logical in
-    if not (DirPath.equal coq_path dir)
-      (* If this is not the default -I . to coqtop *)
-      && not
-      (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
-          && DirPath.equal coq_path (Nameops.default_root_prefix))
-    then
+  | [{ path_logical = old_path; path_implicit = old_implicit }] ->
+    let replace =
+      if DirPath.equal coq_path old_path then
+        implicit <> old_implicit
+      else if DirPath.equal coq_path (Nameops.default_root_prefix)
+              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
+        false (* This is the default "-I ." path, don't override the old path *)
+      else
+        let () =
+          (* Do not warn when overriding the default "-I ." path *)
+          if not (DirPath.equal old_path Nameops.default_root_prefix) then
+            msg_warning
+              (str phys_path ++ strbrk " was previously bound to " ++
+                 pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+                 pr_dirpath coq_path) in
+        true in
+    if replace then
       begin
-        (* Assume the user is concerned by library naming *)
-        if not (DirPath.equal dir Nameops.default_root_prefix) then
-          msg_warning
-            (str phys_path ++ strbrk " was previously bound to " ++
-              pr_dirpath dir ++ strbrk "; it is remapped to " ++
-              pr_dirpath coq_path);
         remove_load_path phys_path;
         load_paths := binding :: !load_paths;
       end
@@ -89,47 +90,25 @@ let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
     (List.rev_map Id.to_string (DirPath.repr dir))
 
-let expand_root_path dir =
+let filter_path f =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then
-      let suffix = drop_dirpath_prefix p.path_logical dir in
-      extend_path_with_dirpath p.path_physical suffix :: aux l
+    if f p.path_logical then (p.path_physical, p.path_logical) :: aux l
     else aux l
   in
   aux !load_paths
 
-(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
-(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
-
-(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
-(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *)
-
-let intersections d1 d2 =
-  let rec aux d1 =
-    if DirPath.is_empty d1 then [d2] else
-      let rest = aux (snd (chop_dirpath 1 d1)) in
-      if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
-      else rest in
-  aux d1
-
-let expand p dir =
-  let ph = extend_path_with_dirpath p.path_physical dir in
-  let log = append_dirpath p.path_logical dir in
-  (ph, log)
-
 let expand_path dir =
   let rec aux = function
   | [] -> []
-  | p :: l ->
-    match p.path_type with
-    | ImplicitPath -> expand p dir :: aux l
-    | ImplicitRootPath ->
-      let inters = intersections p.path_logical dir in
-      List.map (expand p) inters @ aux l
-    | RootPath ->
-      if is_dirpath_prefix_of p.path_logical dir then
-	expand p (drop_dirpath_prefix p.path_logical dir) :: aux l
-      else aux l in
+  | { path_physical = ph; path_logical = lg; path_implicit = implicit }  :: l ->
+    match implicit with
+    | true ->
+      (** The path is implicit, so that we only want match the logical suffix *)
+      if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l
+    | false ->
+      (** Otherwise we must match exactly *)
+      if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
+  in
   aux !load_paths
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 62dc5d59..3251b8c6 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -15,11 +15,6 @@ open Names
 
 *)
 
-type path_type =
-  | ImplicitPath     (** Can be implicitly appended to a logical path. *)
-  | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *)
-  | RootPath         (** Can only be a prefix of a logical path. *)
-
 type t
 (** Type of loadpath bindings. *)
 
@@ -35,8 +30,8 @@ val get_load_paths : unit -> t list
 val get_paths : unit -> CUnix.physical_path list
 (** Same as [get_load_paths] but only get the physical part. *)
 
-val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit
-(** [add_load_path phys type log] adds the binding [phys := log] to the current
+val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
+(** [add_load_path phys log type] adds the binding [phys := log] to the current
     loadpaths. *)
 
 val remove_load_path : CUnix.physical_path -> unit
@@ -52,7 +47,8 @@ val is_in_load_paths : CUnix.physical_path -> bool
 
 val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 (** Given a relative logical path, associate the list of absolute physical and
-    logical paths which are possible expansions of it. *)
+    logical paths which are possible matches of it. *)
 
-val expand_root_path : DirPath.t -> CUnix.physical_path list
-(** As [expand_path] but restricts to root loadpaths. *)
+val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
+(** As {!expand_path} but uses a filter function instead, and ignores the
+    implicit status of loadpaths. *)
diff --git a/library/states.ml b/library/states.ml
index a1c2a095..96a487b1 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,6 +12,7 @@ open System
 type state = Lib.frozen * Summary.frozen
 
 let summary_of_state = snd
+let replace_summary (lib,_) s = lib, s
 
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
diff --git a/library/states.mli b/library/states.mli
index 66de1490..4d5d63e0 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
 val summary_of_state : state -> Summary.frozen
+val replace_summary : state -> Summary.frozen -> state
 
 (** {6 Rollback } *)
 
diff --git a/library/summary.ml b/library/summary.ml
index 7e7628a1..8e2abbf1 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -66,6 +66,7 @@ let freeze_summaries ~marshallable : frozen =
   let fold id (_, decl) accu =
     (* to debug missing Lazy.force
     if marshallable <> `No then begin
+      let id, _ = Int.Map.find id !summaries in
       prerr_endline ("begin marshalling " ^ id);
       ignore(Marshal.to_string (decl.freeze_function marshallable) []);
       prerr_endline ("end marshalling " ^ id);
diff --git a/library/universes.ml b/library/universes.ml
index 79070763..9fddc706 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -165,7 +165,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts 
+      Constr.compare_head_gen_leq eq_universes leq_sorts 
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
@@ -213,7 +213,7 @@ let leq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
@@ -772,7 +772,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	      else 
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
-		with Option.IsNone -> assert false)
+		with Option.IsNone -> failwith "")
 	      cstrs dangling
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
@@ -784,7 +784,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	  | None -> (* Nothing to do *)
 	    acc' (acc, (true, false, Universe.make u))
 	  | Some lbound ->
-	    acc' (instantiate_lbound lbound)
+	     try acc' (instantiate_lbound lbound) 
+	     with Failure _ -> acc' (acc, (true, false, Universe.make u))
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
diff --git a/library/universes.mli b/library/universes.mli
index f2f68d32..252648d7 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -7,12 +7,9 @@
 (************************************************************************)
 
 open Util
-open Pp
 open Names
 open Term
-open Context
 open Environ
-open Locus
 open Univ
 
 (** Universes *)