Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

12 files changed, 326 insertions, 274 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 8f2525b8..d6dfbb6b 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: decl_kinds.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
 
 open Util
 open Libnames
@@ -112,3 +112,18 @@ let strength_of_global = function
 let string_of_strength = function
   | Local -> "Local"
   | Global -> "Global"
+
+
+(* Recursive power *)
+
+(* spiwack: this definition might be of use in the kernel, for now I do not
+                   push them deeper than needed, though. *)
+type recursivity_kind =
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+let recursivity_flag_of_kind = function
+  | Finite | BiFinite -> true
+  | CoFinite -> false
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 9358c4b5..70c63c39 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.mli 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: decl_kinds.mli 11809 2009-01-20 11:39:55Z aspiwack $ *)
 
 open Util
 open Libnames
@@ -82,3 +82,13 @@ val string_of_definition_kind :
 
 val strength_of_global : global_reference -> locality
 val string_of_strength : locality -> string
+
+(* About recursive power of type declarations *)
+
+type recursivity_kind =
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+val recursivity_flag_of_kind : recursivity_kind -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b630b5dc..de1893c7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11246 2008-07-22 15:10:05Z soubiran $ i*)
+(*i $Id: declaremods.ml 11703 2008-12-18 15:54:41Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -151,37 +151,60 @@ let check_subtypes mp sub_mtb =
   in
     ()  (* The constraints are checked and forgot immediately! *) 
 
-let subst_substobjs dir mp (subst,mbids,msid,objs) =
+let compute_subst_objects mp (subst,mbids,msid,objs) =
   match mbids with
-    | [] -> 
+  | [] -> 
+      let subst' = join_alias (map_msid msid mp) subst in
+      Some (join (map_msid msid mp) (join subst' subst), objs)
+  | _ ->
+      None
+
+let subst_substobjs dir mp substobjs =
+  match compute_subst_objects mp substobjs with
+  | Some (subst, objs) ->
 	let prefix = dir,(mp,empty_dirpath) in
-	let subst' = join_alias (map_msid msid mp) subst in
-	let subst = join subst' subst in
-	  Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
-    | _ -> None
+	Some (subst_objects prefix subst objs)
+  | None -> None
+
+(* These functions register the visibility of the module and iterates
+   through its components. They are called by plenty module functions *)
+
+let compute_visibility exists what i dir dirinfo =
+  if exists then 
+    if 
+      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
+      with Not_found -> false 
+    then
+      Nametab.Exactly i
+    else
+      errorlabstrm (what^"_module")
+	(pr_dirpath dir ++ str " should already exist!") 
+  else
+    if Nametab.exists_dir dir then
+      errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+    else
+      Nametab.Until i
 
-(* This function registers the visibility of the module and iterates
-   through its components. It is called by plenty module functions *)
+let do_load_and_subst_module i dir mp substobjs keep =
+  let prefix = (dir,(mp,empty_dirpath)) in
+  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+  let vis = compute_visibility false "load_and_subst" i dir dirinfo in
+  let objects = compute_subst_objects mp substobjs in
+  Nametab.push_dir vis dir dirinfo;
+  modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+  match objects with
+  | Some (subst,seg) ->
+      let seg = load_and_subst_objects (i+1) prefix subst seg in
+      modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+      load_objects (i+1) prefix keep;
+      Some (seg@keep)
+  | None ->
+      None
 
 let do_module exists what iter_objects i dir mp substobjs objects =
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = 
-    if exists then 
-      if 
-	try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-	with Not_found -> false 
-      then
-	Nametab.Exactly i
-      else
-	errorlabstrm (what^"_module") 
-	  (pr_dirpath dir ++ str " should already exist!") 
-    else
-      if Nametab.exists_dir dir then
-	errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
-      else
-	Nametab.Until i
-  in
+  let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
     match objects with
@@ -324,22 +347,7 @@ and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
     try Some (MPmap.find alias !modtab_objects) with
 	Not_found -> None in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = 
-    if exists then 
-      if 
-	try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-	with Not_found -> false 
-      then
-	Nametab.Exactly i
-      else
-	errorlabstrm (what^"_module") 
-	  (pr_dirpath dir ++ str " should already exist!") 
-    else
-      if Nametab.exists_dir dir then
-	errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
-      else
-	Nametab.Until i
-  in
+  let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
     match alias_objects,objects with
@@ -588,16 +596,21 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
       let rec replace_idl = function 
 	| _,[] -> [] 
 	| id::idl,(id',obj)::tail when id = id' ->
-	    if object_tag obj = "MODULE" then
+	    let tag = object_tag obj in
+	    if tag = "MODULE" or tag ="MODULE ALIAS" then
               (match idl with
 		   [] -> (id, in_module_alias (Some
 						 ({mod_entry_type = None;
 						   mod_entry_expr = Some (MSEident mp)},None)
 						 ,modobjs,None))::tail
 		 | _ ->
-		     let (_,substobjs,_) = out_module obj in
+		     let (a,substobjs,_) = if tag =  "MODULE ALIAS" then
+		       out_module_alias obj else out_module obj in
                      let substobjs' = replace_module_object idl substobjs modobjs mp in
-                       (id, in_module (None,substobjs',None))::tail
+  		       if tag =  "MODULE ALIAS" then
+			 (id, in_module_alias (a,substobjs',None))::tail
+		       else
+			 (id, in_module (None,substobjs',None))::tail
               )
 	    else error "MODULE expected!"
 	| idl,lobj::tail -> lobj::replace_idl (idl,tail)
@@ -645,8 +658,8 @@ let rec get_modtype_substobjs env = function
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
 		((join 
-		    (join subst (map_mbid mbid mp (Some resolve)))
-		       sub3)
+		    (join subst sub3)
+		    (map_mbid mbid mp (Some resolve)))
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
@@ -662,8 +675,7 @@ let process_module_bindings argids args =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
     let substobjs = get_modtype_substobjs (Global.env()) mty in
-    let substituted = subst_substobjs dir mp substobjs in
-      do_module false "start" load_objects 1 dir mp substobjs substituted
+    ignore (do_load_and_subst_module 1 dir mp substobjs [])
   in
     List.iter2 process_arg argids args
 
@@ -677,8 +689,7 @@ let intern_args interp_modtype (idl,arg) =
     (fun dir mbid -> 
       Global.add_module_parameter mbid mty;
       let mp = MPbound mbid in
-      let substituted = subst_substobjs dir mp substobjs in
-      do_module false "interp" load_objects 1 dir mp substobjs substituted;
+      ignore (do_load_and_subst_module 1 dir mp substobjs []);
       (mbid,mty))
     dirs mbids
 
@@ -792,25 +803,19 @@ type library_objects =
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let substobjs, objects =
-    try 
-      ignore(Global.lookup_module mp);
-      (* if it's in the environment, the cached objects should be correct *)
-      Dirmap.find dir !library_cache 
-    with
-	Not_found ->
-	  if mp <> Global.import cenv digest then
-	    anomaly "Unexpected disk module name";
-	  let msid,substitute,keep = objs in
-	  let substobjs = empty_subst, [], msid, substitute in
-	  let substituted = subst_substobjs dir mp substobjs in
-	  let objects = Option.map (fun seg -> seg@keep) substituted in
-	  let modobjs = substobjs, objects in
-	    library_cache := Dirmap.add dir modobjs !library_cache;
-	    modobjs
-  in
+  try 
+    ignore(Global.lookup_module mp);
+    (* if it's in the environment, the cached objects should be correct *)
+    let substobjs, objects = Dirmap.find dir !library_cache in
     do_module false "register_library" load_objects 1 dir mp substobjs objects
-
+  with Not_found ->
+    if mp <> Global.import cenv digest then
+      anomaly "Unexpected disk module name";
+    let msid,substitute,keep = objs in
+    let substobjs = empty_subst, [], msid, substitute in
+    let objects = do_load_and_subst_module 1 dir mp substobjs keep in
+    let modobjs = substobjs, objects in
+    library_cache := Dirmap.add dir modobjs !library_cache
 
 let start_library dir = 
   let mp = Global.start_library dir in
@@ -960,8 +965,8 @@ let rec get_module_substobjs env = function
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
 		((join 
-		    (join subst (map_mbid mbid mp (Some resolve)))
-		       sub3)
+		    (join subst sub3)
+		       (map_mbid mbid mp (Some resolve)))
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
diff --git a/library/impargs.ml b/library/impargs.ml
index 3a505ddb..2b2c607c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 open Util
 open Names
@@ -71,6 +71,7 @@ let make_maximal_implicit_args flag =
 
 let is_implicit_args () = !implicit_args.main
 let is_manual_implicit_args () = !implicit_args.manual
+let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -577,10 +578,11 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool)
 let compute_implicits_with_manual env typ enriching l = 
   compute_manual_implicits env !implicit_args typ enriching l
 
-let declare_manual_implicits local ref enriching l =
+let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
+  let enriching = Option.default (is_auto_implicit_args ()) enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if local or isVarRef ref then ImplLocal
@@ -588,9 +590,9 @@ let declare_manual_implicits local ref enriching l =
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
-let maybe_declare_manual_implicits local ref enriching l =
+let maybe_declare_manual_implicits local ref ?enriching l =
   if l = [] then ()
-  else declare_manual_implicits local ref enriching l
+  else declare_manual_implicits local ref ?enriching l
 
 let lift_implicits n = 
   List.map (fun x -> 
diff --git a/library/impargs.mli b/library/impargs.mli
index 705efd31..a363effa 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -83,14 +83,16 @@ val declare_implicits : bool -> global_reference -> unit
 
 (* [declare_manual_implicits local ref enriching l]
    Manual declaration of which arguments are expected implicit.
+   If not set, we decide if it should enrich by automatically inferd
+   implicits depending on the current state.
    Unsets implicits if [l] is empty. *)
 
-val declare_manual_implicits : bool -> global_reference -> bool ->
+val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
   manual_explicitation list -> unit
 
 (* If the list is empty, do nothing, otherwise declare the implicits. *)
 
-val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
   manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
diff --git a/library/lib.ml b/library/lib.ml
index fa71bb2f..88bcd0b8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,11 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
 
 open Pp
 open Util
-open Names
 open Libnames
 open Nameops
 open Libobject
@@ -33,7 +32,7 @@ and library_entry = object_name * node
 
 and library_segment = library_entry list
 
-type lib_objects =  (identifier * obj) list
+type lib_objects =  (Names.identifier * obj) list
 
 let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
@@ -49,11 +48,18 @@ let subst_objects prefix subst seg =
   in
     list_smartmap subst_one seg
 
+let load_and_subst_objects i prefix subst seg =
+  List.rev (List.fold_left (fun seg (id,obj as node) ->
+    let obj' =  subst_object (make_oname prefix id, subst, obj) in
+    let node = if obj == obj' then node else (id, obj') in
+    load_object i (make_oname prefix id, obj');
+    node :: seg) [] seg)
+
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn as oname),Leaf o) :: stk -> 
-	let id = id_of_label (label kn) in
+	let id = Names.id_of_label (Names.label kn) in
 	  (match classify_object (oname,o) with 
 	     | Dispose -> clean acc stk
 	     | Keep o' -> 
@@ -85,7 +91,7 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *) 
 
-let initial_prefix = default_library,(initial_path,empty_dirpath)
+let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
 
 let lib_stk = ref ([] : library_segment)
 
@@ -98,8 +104,21 @@ let library_dp () =
    module path and relative section path *)
 let path_prefix = ref initial_prefix
 
+let sections_depth () =
+  List.length (Names.repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+  match Names.repr_dirpath (snd (snd !path_prefix)) with
+      [] -> false
+    | _ -> true
+
 let cwd () = fst !path_prefix
 
+let current_dirpath sec =
+  Libnames.drop_dirpath_prefix (library_dp ()) 
+    (if sec then cwd () 
+      else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
+    
 let make_path id = Libnames.make_path (cwd ()) id
 
 let path_of_include () =
@@ -112,25 +131,15 @@ let current_prefix () = snd !path_prefix
 
 let make_kn id = 
   let mp,dir = current_prefix () in
-    Names.make_kn mp dir (label_of_id id)
+    Names.make_kn mp dir (Names.label_of_id id)
 
 let make_con id = 
   let mp,dir = current_prefix () in
-    Names.make_con mp dir (label_of_id id)
+    Names.make_con mp dir (Names.label_of_id id)
 
 
 let make_oname id = make_path id, make_kn id
 
-
-let sections_depth () =
-  List.length (repr_dirpath (snd (snd !path_prefix)))
-
-let sections_are_opened () =
-  match repr_dirpath (snd (snd !path_prefix)) with
-      [] -> false
-    | _ -> true
-
-
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection (dir,_)) :: _ -> dir
@@ -194,7 +203,7 @@ let add_entry sp node =
 
 let anonymous_id = 
   let n = ref 0 in
-  fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+  fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
   let id = anonymous_id () in
@@ -207,7 +216,7 @@ let add_absolutely_named_leaf sp obj =
   add_entry sp (Leaf obj)
 
 let add_leaf id obj =
-  if fst (current_prefix ()) = initial_path then 
+  if fst (current_prefix ()) = Names.initial_path then 
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -261,7 +270,7 @@ let current_mod_id () =
 
 let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
-  let prefix = dir,(mp,empty_dirpath) in
+  let prefix = dir,(mp,Names.empty_dirpath) in
   let oname = make_path id, make_kn id in
   if Nametab.exists_module dir then
     errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
@@ -306,7 +315,7 @@ let end_module id =
 
 let start_modtype id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
-  let prefix = dir,(mp,empty_dirpath) in
+  let prefix = dir,(mp,Names.empty_dirpath) in
   let sp = make_path id in
   let name = sp, make_kn id in
   if Nametab.exists_cci sp then
@@ -363,9 +372,9 @@ let check_for_comp_unit () =
 let start_compilation s mp =
   if !comp_name <> None then
     error "compilation unit is already started";
-  if snd (snd (!path_prefix)) <> empty_dirpath then
+  if snd (snd (!path_prefix)) <> Names.empty_dirpath then
     error "some sections are already opened";
-  let prefix = s, (mp, empty_dirpath) in
+  let prefix = s, (mp, Names.empty_dirpath) in
   let _ = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
@@ -395,8 +404,8 @@ let end_compilation dir =
       | None -> anomaly "There should be a module name..."
       | Some m ->
 	  if m <> dir then anomaly 
-	    ("The current open module has name "^ (string_of_dirpath m) ^ 
-	       " and not " ^ (string_of_dirpath m));
+	    ("The current open module has name "^ (Names.string_of_dirpath m) ^ 
+	       " and not " ^ (Names.string_of_dirpath m));
   in
   let (after,_,before) = split_lib oname in
     comp_name := None;
@@ -446,7 +455,7 @@ let sectab =
   ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
-  sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+  sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
 
 let add_section_variable id impl keep =
   match !sectab with
@@ -489,10 +498,10 @@ let replacement_context () = pi2 (List.hd !sectab)
 let variables_context () = pi1 (List.hd !sectab)
 
 let section_segment_of_constant con =
-  Cmap.find con (fst (pi3 (List.hd !sectab)))
+  Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
 let section_segment_of_mutual_inductive kn =
-  KNmap.find kn (snd (pi3 (List.hd !sectab)))
+  Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
 let rec list_mem_assoc_in_triple x = function
     [] -> raise Not_found
@@ -503,9 +512,9 @@ let section_instance = function
       if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
       else raise Not_found
   | ConstRef con ->
-      Cmap.find con (fst (pi2 (List.hd !sectab)))
+      Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      KNmap.find kn (snd (pi2 (List.hd !sectab)))
+      Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
@@ -566,11 +575,11 @@ let close_section id =
       | oname,OpenedSection (_,fs) -> 
 	  let id' = basename (fst oname) in 
 	    if id <> id' then 
-	      errorlabstrm "close_section" (str "last opened section is " ++ pr_id id');
+	      errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
 	    (oname,fs)
       | _ -> assert false 
     with Not_found ->
-      error "no opened section"
+      error "No opened section."
   in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
@@ -730,7 +739,7 @@ let back n = reset_to (back_stk n !lib_stk)
 
 (* State and initialization. *)
 
-type frozen = dir_path option * library_segment
+type frozen = Names.dir_path option * library_segment
 
 let freeze () = (!comp_name, !lib_stk)
 
@@ -774,16 +783,37 @@ let reset_initial () =
 let mp_of_global ref = 
   match ref with
     | VarRef id -> fst (current_prefix ())
-    | ConstRef cst -> con_modpath cst
-    | IndRef ind -> ind_modpath ind
-    | ConstructRef constr -> constr_modpath constr
+    | ConstRef cst -> Names.con_modpath cst
+    | IndRef ind -> Names.ind_modpath ind
+    | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp modp =
   match modp with
-    | MPfile dp -> dp
-    | MPbound _ | MPself _ -> library_dp ()
-    | MPdot (mp,_) -> dp_of_mp mp
-
+    | Names.MPfile dp -> dp
+    | Names.MPbound _ | Names.MPself _ -> library_dp ()
+    | Names.MPdot (mp,_) -> dp_of_mp mp
+
+let rec split_mp mp = 
+  match mp with 
+    | Names.MPfile dp -> dp,  Names.empty_dirpath
+    | Names.MPdot (prfx, lbl) -> 
+	let mprec, dprec = split_mp prfx in 
+	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
+    | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+
+let split_modpath mp =
+  let rec aux = function
+    | Names.MPfile dp -> dp, []
+    | Names.MPbound mbid -> 
+	library_dp (), [Names.id_of_mbid mbid]
+    | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
+    | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
+			      (mp', Names.id_of_label l :: lab)
+  in 
+  let (mp, l) = aux mp in
+    mp, l
+			
 let library_part ref =
   match ref with 
     | VarRef id -> library_dp ()
@@ -815,12 +845,12 @@ let pop_con con =
   Names.make_con mp (dirpath_prefix dir) l
 
 let con_defined_in_sec kn = 
-  let _,dir,_ = repr_con kn in
-  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  let _,dir,_ = Names.repr_con kn in
+  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let defined_in_sec kn = 
-  let _,dir,_ = repr_kn kn in
-  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  let _,dir,_ = Names.repr_kn kn in
+  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/lib.mli b/library/lib.mli
index d35fcc09..23af7c17 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,41 +6,34 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
 
-(*i*)
-open Util
-open Names
-open Libnames
-open Libobject
-open Summary
-open Mod_subst
-(*i*)
 
 (*s This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
 
 type node = 
-  | Leaf of obj
-  | CompilingLibrary of object_prefix
-  | OpenedModule of bool option * object_prefix * Summary.frozen
+  | Leaf of Libobject.obj
+  | CompilingLibrary of Libnames.object_prefix
+  | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
   | ClosedModule  of library_segment
-  | OpenedModtype of object_prefix * Summary.frozen
+  | OpenedModtype of Libnames.object_prefix * Summary.frozen
   | ClosedModtype of library_segment
-  | OpenedSection of object_prefix * Summary.frozen
+  | OpenedSection of Libnames.object_prefix * Summary.frozen
   | ClosedSection of library_segment
   | FrozenState of Summary.frozen
 
-and library_segment = (object_name * node) list
+and library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * Libobject.obj) list
 
 (*s Object iteratation functions. *)
 
-val open_objects : int -> object_prefix -> lib_objects -> unit
-val load_objects : int -> object_prefix -> lib_objects -> unit
-val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
+val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
 
 (* [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
@@ -48,23 +41,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
    [Substitute], [Keep], [Anticipate] respectively.  The order of each
    returned list is the same as in the input list. *)
 val classify_segment : 
-  library_segment -> lib_objects * lib_objects * obj list
+  library_segment -> lib_objects * lib_objects * Libobject.obj list
 
 (* [segment_of_objects prefix objs] forms a list of Leafs *)
 val segment_of_objects :
-  object_prefix -> lib_objects -> library_segment
+  Libnames.object_prefix -> lib_objects -> library_segment
 
 
 (*s Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : identifier -> obj -> object_name
-val add_absolutely_named_leaf : object_name -> obj -> unit
-val add_anonymous_leaf : obj -> unit
+val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
+val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit
+val add_anonymous_leaf : Libobject.obj -> unit
 
 (* this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-val add_leaves : identifier -> obj list -> object_name
+val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
@@ -81,19 +74,20 @@ val reset_label : int -> unit
   starting from a given section path. If not given, the entire segment
   is returned. *)
 
-val contents_after : object_name option -> library_segment
+val contents_after : Libnames.object_name option -> library_segment
 
 (*s Functions relative to current path *)
 
 (* User-side names *)
-val cwd : unit -> dir_path
-val make_path : identifier -> section_path
-val path_of_include : unit -> section_path
+val cwd : unit -> Names.dir_path
+val current_dirpath : bool -> Names.dir_path
+val make_path : Names.identifier -> Libnames.section_path
+val path_of_include : unit -> Libnames.section_path
 
 (* Kernel-side names *)
-val current_prefix : unit -> module_path * dir_path
-val make_kn : identifier -> kernel_name
-val make_con : identifier -> constant
+val current_prefix : unit -> Names.module_path * Names.dir_path
+val make_kn : Names.identifier -> Names.kernel_name
+val make_con : Names.identifier -> Names.constant
 
 (* Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -102,53 +96,55 @@ val sections_depth : unit -> int
 (* Are we inside an opened module type *)
 val is_modtype : unit -> bool
 val is_module : unit -> bool
-val current_mod_id : unit -> module_ident
+val current_mod_id : unit -> Names.module_ident
 
 (* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> object_name * node
+val what_is_opened : unit -> Libnames.object_name * node
 
 
 (*s Modules and module types *)
 
 val start_module : 
-  bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_module : module_ident 
-  -> object_name * object_prefix * Summary.frozen * library_segment
+  bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_module : Names.module_ident 
+  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 
 val start_modtype : 
-  module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_modtype : module_ident 
-  -> object_name * object_prefix * Summary.frozen * library_segment
+  Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_modtype : Names.module_ident 
+  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 (* [Lib.add_frozen_state] must be called after each of the above functions *)
 
 (*s Compilation units *)
 
-val start_compilation : dir_path -> module_path -> unit
-val end_compilation : dir_path -> object_prefix * library_segment
+val start_compilation : Names.dir_path -> Names.module_path -> unit
+val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment
 
 (* The function [library_dp] returns the [dir_path] of the current
    compiling library (or [default_library]) *)
-val library_dp : unit -> dir_path
+val library_dp : unit -> Names.dir_path
 
 (* Extract the library part of a name even if in a section *)
-val dp_of_mp : module_path -> dir_path
-val library_part :  global_reference -> dir_path
-val remove_section_part : global_reference -> dir_path
+val dp_of_mp : Names.module_path -> Names.dir_path
+val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
+val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val library_part :  Libnames.global_reference -> Names.dir_path
+val remove_section_part : Libnames.global_reference -> Names.dir_path
 
 (*s Sections *)
 
-val open_section : identifier -> unit
-val close_section : identifier -> unit
+val open_section : Names.identifier -> unit
+val close_section : Names.identifier -> unit
 
 (*s Backtracking (undo). *)
 
-val reset_to : object_name -> unit
-val reset_name : identifier located -> unit
-val remove_name : identifier located -> unit
-val reset_mod : identifier located -> unit
-val reset_to_state : object_name -> unit
+val reset_to : Libnames.object_name -> unit
+val reset_name : Names.identifier Util.located -> unit
+val remove_name : Names.identifier Util.located -> unit
+val reset_mod : Names.identifier Util.located -> unit
+val reset_to_state : Libnames.object_name -> unit
 
-val has_top_frozen_state : unit -> object_name option
+val has_top_frozen_state : unit -> Libnames.object_name option
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)
@@ -168,8 +164,8 @@ val reset_initial : unit -> unit
 
 
 (* XML output hooks *)
-val set_xml_open_section : (identifier -> unit) -> unit
-val set_xml_close_section : (identifier -> unit) -> unit
+val set_xml_open_section : (Names.identifier -> unit) -> unit
+val set_xml_close_section : (Names.identifier -> unit) -> unit
 
 type binding_kind = Explicit | Implicit
 
@@ -190,13 +186,13 @@ val add_section_variable : Names.identifier -> binding_kind -> Term.types option
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (identifier array Cmap.t * identifier array KNmap.t)
+  (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
 
 (*s Discharge: decrease the section level if in the current section *)
 
-val discharge_kn :  kernel_name -> kernel_name
-val discharge_con : constant -> constant
-val discharge_global : global_reference -> global_reference
-val discharge_inductive : inductive -> inductive
+val discharge_kn :  Names.kernel_name -> Names.kernel_name
+val discharge_con : Names.constant -> Names.constant
+val discharge_global : Libnames.global_reference -> Libnames.global_reference
+val discharge_inductive : Names.inductive -> Names.inductive
 
 
diff --git a/library/libnames.ml b/library/libnames.ml
index d0c6e8b9..3f226179 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: libnames.ml 11750 2009-01-05 20:47:34Z herbelin $ i*)
 
 open Pp
 open Util
@@ -24,6 +24,11 @@ type global_reference =
 
 let isVarRef = function VarRef _ -> true | _ -> false
 
+let subst_constructor subst ((kn,i),j as ref) =
+  let kn' = subst_kn subst kn in 
+    if kn==kn' then ref, mkConstruct ref
+    else ((kn',i),j), mkConstruct ((kn',i),j)
+      
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
@@ -32,10 +37,9 @@ let subst_global subst ref = match ref with
   | IndRef (kn,i) ->
       let kn' = subst_kn subst kn in
       if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
-  | ConstructRef ((kn,i),j) ->
-      let kn' = subst_kn subst kn in 
-      if kn==kn' then ref, mkConstruct ((kn,i),j)
-      else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
+  | ConstructRef ((kn,i),j as c) ->
+      let c',t = subst_constructor subst c in
+	if c'==c then ref,t else ConstructRef c', t
 
 let global_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
@@ -119,21 +123,21 @@ let path_of_inductive env (sp,tyi) =
 let parse_dir s =
   let len = String.length s in
   let rec decoupe_dirs dirs n =
-    if n>=len then dirs else
+    if n = len && n > 0 then error (s ^ " is an invalid path.");
+    if n >= len then dirs else
     let pos =
       try
 	String.index_from s n '.' 
       with Not_found -> len
     in
+    if pos = n then error (s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
-      decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
+    decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
   in
     decoupe_dirs [] 0
 
-let dirpath_of_string s = 
-  match parse_dir s with
-      [] -> invalid_arg "dirpath_of_string"
-    | dir -> make_dirpath dir
+let dirpath_of_string s =
+  make_dirpath (if s = "" then [] else parse_dir s)
 
 module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
 module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
diff --git a/library/libnames.mli b/library/libnames.mli
index 76c406db..cc664a08 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: libnames.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 (*i*)
 open Pp
@@ -25,6 +25,7 @@ type global_reference =
 
 val isVarRef : global_reference -> bool
 
+val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 6b302447..b455e2b3 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: libobject.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
 
 open Util
 open Names
@@ -148,8 +148,9 @@ let apply_dyn_fun deflt f lobj =
 	  if !relax_flag then
 	    failwith "local to_apply_dyn_fun"
 	  else
-	    anomaly
-	      ("Cannot find library functions for an object with tag "^tag) in 
+	    error
+	      ("Cannot find library functions for an object with tag "^tag^
+	       " (maybe a plugin is missing)") in 
 	f dodecl
     with
 	Failure "local to_apply_dyn_fun" -> deflt;;
diff --git a/library/library.ml b/library/library.ml
index 73928a9b..9f3478f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11313 2008-08-07 11:15:03Z barras $ *)
+(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
 
 open Pp
 open Util
@@ -18,7 +18,6 @@ open Safe_typing
 open Libobject
 open Lib
 open Nametab
-open Declaremods
 
 (*************************************************************************)
 (*s Load path. Mapping from physical to logical paths etc.*)
@@ -29,43 +28,15 @@ let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
 
 let get_load_paths () = List.map pi1 !load_paths
 
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p = 
-  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
-  let n = String.length curdir in
-  if String.length p > n && String.sub p 0 n = curdir then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    p
-
-let strip_path p =
-  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
-  let n = String.length cwd in
-  if String.length p > n && String.sub p 0 n = cwd then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    remove_path_dot p
-
-let canonical_path_name p =
-  let current = Sys.getcwd () in
-  try 
-    Sys.chdir p;
-    let p' = Sys.getcwd () in
-    Sys.chdir current;
-    p'
-  with Sys_error _ ->
-    (* We give up to find a canonical name and just simplify it... *)
-    strip_path p
-
 let find_logical_path phys_dir =
-  let phys_dir = canonical_path_name phys_dir in
+  let phys_dir = System.canonical_path_name phys_dir in
   match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
   | [_,dir,_] -> dir
   | [] -> Nameops.default_root_prefix
   | l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let is_in_load_paths phys_dir =
-  let dir = canonical_path_name phys_dir in
+  let dir = System.canonical_path_name phys_dir in
   let lp = get_load_paths () in
   let check_p = fun p -> (String.compare dir p) == 0 in
     List.exists check_p lp 
@@ -74,13 +45,13 @@ let remove_load_path dir =
   load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
 
 let add_load_path isroot (phys_path,coq_path) =
-  let phys_path = canonical_path_name phys_path in
+  let phys_path = System.canonical_path_name phys_path in
     match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
       | [_,dir,_] ->
 	  if coq_path <> dir 
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = canonical_path_name Filename.current_dir_name
+            (phys_path = System.canonical_path_name Filename.current_dir_name
 		&& coq_path = Nameops.default_root_prefix)
 	  then
 	    begin
@@ -149,7 +120,7 @@ type compilation_unit_name = dir_path
 type library_disk = { 
   md_name : compilation_unit_name;
   md_compiled : compiled_library;
-  md_objects : library_objects;
+  md_objects : Declaremods.library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
 
@@ -159,7 +130,7 @@ type library_disk = {
 type library_t = {
   library_name : compilation_unit_name;
   library_compiled : compiled_library;
-  library_objects : library_objects;
+  library_objects : Declaremods.library_objects;
   library_deps : (compilation_unit_name * Digest.t) list;
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
@@ -324,14 +295,14 @@ let open_libraries export modl =
 (**********************************************************************)
 (* import and export  -  synchronous operations*)
 
-let cache_import (_,(dir,export)) = 
-  open_libraries export [try_find_library dir]
-
-let open_import i (_,(dir,_) as obj) =
+let open_import i (_,(dir,export)) =
   if i=1 then
     (* even if the library is already imported, we re-import it *)
     (* if not (library_is_opened dir) then *)
-      cache_import obj
+      open_libraries export [try_find_library dir]
+
+let cache_import obj = 
+  open_import 1 obj
 
 let subst_import (_,_,o) = o
 
@@ -379,7 +350,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = (string_of_id base)^".vo" in
-    let _, file = System.where_in_path false loadpath name in
+    let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -395,7 +366,7 @@ let locate_qualified_library warn qid =
     let loadpath = loadpaths_matching_dir_path dir in
     if loadpath = [] then raise LibUnmappedDir;
     let name = string_of_id base ^ ".vo" in
-    let lpath, file = System.where_in_path warn (List.map fst loadpath) name in
+    let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
     let dir = extend_dirpath (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
@@ -506,12 +477,14 @@ let rec_intern_by_filename_only id f =
 
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
-  let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
+  let paths = get_load_paths () in
+  let _, f = 
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
-(*s [require_library] loads and opens a library. This is a synchronized
-    operation. It is performed as follows:
+(*s [require_library] loads and possibly opens a library. This is a 
+    synchronized operation. It is performed as follows:
 
   preparation phase: (functions require_library* ) the library and its 
     dependencies are read from to disk (using intern_* )
@@ -524,10 +497,6 @@ let rec_intern_library_from_file idopt f =
     the library is loaded in the environment and Nametab, the objects are 
     registered etc, using functions from Declaremods (via load_library, 
     which recursively loads its dependencies)
-
-
-  The [read_library] operation is very similar, but does not "open"
-    the library
 *)
 
 type library_reference = dir_path list * bool option
@@ -540,14 +509,21 @@ let register_library (dir,m) =
     m.library_digest;
   register_loaded_library m
 
-  (* [needed] is the ordered list of libraries not already loaded *)
-let cache_require (_,(needed,modl,export)) =
-  List.iter register_library needed;
+(* Follow the semantics of Anticipate object:
+   - called at module or module type closing when a Require occurs in 
+     the module or module type
+   - not called from a library (i.e. a module identified with a file) *)
+let load_require _ (_,(needed,modl,_)) =
+  List.iter register_library needed
+
+let open_require i (_,(_,modl,export)) =
   Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
     export
 
-let load_require  _ (_,(needed,modl,_)) =
-  List.iter register_library needed
+  (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require o =
+  load_require 1 o;
+  open_require 1 o
 
   (* keeps the require marker for closed section replay but removes
      OS dependent fields from .vo files for cross-platform compatibility *)
@@ -555,10 +531,13 @@ let export_require (_,l,e) = Some ([],l,e)
 
 let discharge_require (_,o) = Some o
 
+(* open_function is never called from here because an Anticipate object *) 
+
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
+       open_function = (fun _ _ -> assert false);
        export_function = export_require;
        discharge_function = discharge_require;
        classify_function = (fun (_,o) -> Anticipate o) }
@@ -566,8 +545,6 @@ let (in_require, out_require) =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-(* read = require without opening *)
-
 let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
@@ -575,19 +552,16 @@ let require_library qidl export =
   let modrefl = List.map try_locate_qualified_library qidl in
   let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
   let modrefl = List.map fst modrefl in
-    if Lib.is_modtype () || Lib.is_module () then 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)
-	export
-    end
+    if Lib.is_modtype () || Lib.is_module () then 
+      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)
+	  export
+      end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-  if !Flags.dump then List.iter2 (fun (loc, _) dp -> 
-    Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
-		    (fst (unloc loc)) (string_of_dirpath dp) "lib"))
-    qidl modrefl;
-  if !Flags.xml_export then List.iter !xml_require modrefl;
+    if !Flags.xml_export then List.iter !xml_require modrefl;
   add_frozen_state ()
 
 let require_library_from_file idopt file export =
@@ -608,25 +582,33 @@ let require_library_from_file idopt file export =
 let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
-	MPfile dir -> 
+      | MPfile dir -> 
 	  if Lib.is_modtype () || Lib.is_module () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
-	    add_anonymous_leaf (in_require ([],[dir], Some export))
+	    add_anonymous_leaf (in_import (dir, export))
       | mp ->
-	  import_module 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"))
+          (loc,"import_library",
+	  str ((string_of_qualid qid)^" is not a module"))
   
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
+let check_coq_overwriting p =
+  let l = repr_dirpath p in
+  if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
+    errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
+
 let start_library f = 
-  let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
+  let paths = get_load_paths () in
+  let _,longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
+  check_coq_overwriting ldir0;
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
   Declaremods.start_library ldir;
diff --git a/library/library.mli b/library/library.mli
index a66a77bc..d61dc4b9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: library.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: library.mli 11750 2009-01-05 20:47:34Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -76,6 +76,10 @@ type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
+val try_locate_qualified_library : qualid located -> dir_path * string
+
+(* Reserve Coq prefix for the standard library *)
+val check_coq_overwriting : dir_path -> unit
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds