Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

13 files changed, 157 insertions, 128 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b1e55c20..81401a8e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
+(* $Id: declare.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -204,7 +204,7 @@ let hcons_constant_declaration = function
       let (hcons1_constr,_) = hcons_constr (hcons_names()) in
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
-	 const_entry_type = option_app hcons1_constr ce.const_entry_type;
+	 const_entry_type = option_map hcons1_constr ce.const_entry_type;
          const_entry_opaque = ce.const_entry_opaque; 
          const_entry_boxed = ce.const_entry_boxed }
   | cd -> cd
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3b2196a5..aac2b599 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 7720 2005-12-24 00:25:55Z herbelin $ i*)
+(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
 
 open Pp
 open Util
@@ -122,6 +122,18 @@ let msid_of_prefix (_,(mp,sec)) =
     anomaly ("Non-empty section in module name!" ^ 
 	     string_of_mp mp ^ "." ^ string_of_dirpath sec)
 
+(* Check that a module type is not functorial *)
+
+let rec check_sig env = function
+  | MTBident kn -> check_sig env (Environ.lookup_modtype kn env)
+  | MTBsig _ -> ()
+  | MTBfunsig _ -> Modops.error_result_must_be_signature ()
+
+let rec check_sig_entry env = function
+  | MTEident kn -> check_sig env (Environ.lookup_modtype kn env)
+  | MTEsig _ -> ()
+  | MTEfunsig _ -> Modops.error_result_must_be_signature ()
+  | MTEwith (mte,_) -> check_sig_entry env mte
 
 (* This function checks if the type calculated for the module [mp] is
    a subtype of [sub_mtb]. Uses only the global environment. *)
@@ -434,58 +446,47 @@ let rec get_some_body mty env = match mty with
       replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
 
 
-let intern_args interp_modtype (env,oldargs) (idl,arg) = 
+let intern_args interp_modtype (idl,arg) = 
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
-  let mty = interp_modtype env arg in
+  let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
-  let mps = List.map (fun mbid -> MPbound mbid) mbids in
   let substobjs = get_modtype_substobjs mty in
-  let substituted's = 
-    List.map2 
-      (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) 
-      dirs mps  
-  in
-    List.iter 
-      (fun (dir, mp, substituted) -> 
-	 do_module false "interp" load_objects 1 dir mp substobjs substituted)
-      substituted's;
-    let body = Modops.module_body_of_type (get_some_body mty env) in
-    let env = 
-      List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
-    in
-    env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
-      
+  List.map2
+    (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;
+      (mbid,mty))
+    dirs mbids
+
 let start_module interp_modtype export id args res_o =
   let fs = Summary.freeze_summaries () in
-  let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
-  in
-  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  let mp = Global.start_module id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
   let res_entry_o, sub_body_o = match res_o with
       None -> None, None
-    | Some (res, true) ->
-	Some (interp_modtype env res), None
-    | Some (res, false) ->
-	(* If the module type is non-restricting, we must translate it
-	   here to catch errors as early as possible. If it is
-	   estricting, the kernel takes care of it.  *)
-	let sub_mte = 
-	  List.fold_right 
-	    (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
-	    arg_entries 
-	    (interp_modtype env res)
-	in
-	let sub_mtb = 
-	  Mod_typing.translate_modtype (Global.env()) sub_mte
-	in
+    | Some (res, restricted) ->
+	(* we translate the module here to catch errors as early as possible *)
+	let mte = interp_modtype (Global.env()) res in
+	check_sig_entry (Global.env()) mte;
+	if restricted then
+	  Some mte, None
+	else
+	  let mtb = Mod_typing.translate_modtype (Global.env()) mte in
+	  let sub_mtb = 
+	    List.fold_right 
+	      (fun (arg_id,arg_t) mte -> 
+		let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t
+		in MTBfunsig(arg_id,arg_t,mte))
+	      arg_entries mtb
+	  in
 	  None, Some sub_mtb
   in
 
-  let mp = Global.start_module id arg_entries res_entry_o in
-
   let mbids = List.map fst arg_entries in
   openmod_info:=(mbids,res_entry_o,sub_body_o);
   let prefix = Lib.start_module export id mp fs in
@@ -496,8 +497,8 @@ let start_module interp_modtype export id args res_o =
 let end_module id =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
-  let mp = Global.end_module id in
   let mbids, res_o, sub_o = !openmod_info in
+  let mp = Global.end_module id res_o in
     
   begin match sub_o with
       None -> ()
@@ -584,7 +585,7 @@ let register_library dir cenv objs digest =
 	  let msid,substitute,keep = objs in
 	  let substobjs = empty_subst, [], msid, substitute in
 	  let substituted = subst_substobjs dir mp substobjs in
-	  let objects = option_app (fun seg -> seg@keep) substituted in
+	  let objects = option_map (fun seg -> seg@keep) substituted in
 	  let modobjs = substobjs, objects in
 	    Hashtbl.add library_cache dir modobjs;
 	    modobjs
@@ -644,13 +645,9 @@ let import_module export mp =
 
 let start_modtype interp_modtype id args =
   let fs = Summary.freeze_summaries () in
-  let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
-  in
-  let arg_entries = List.concat (List.rev arg_entries_revlist) in
 
-  let mp = Global.start_modtype id arg_entries in
+  let mp = Global.start_modtype id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
   let mbids = List.map fst arg_entries in
   openmodtype_info := mbids;
@@ -685,12 +682,11 @@ let end_modtype id =
 
 let declare_modtype interp_modtype id args mty = 
   let fs = Summary.freeze_summaries () in
-  let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
-  in
-  let arg_entries = List.concat (List.rev arg_entries_revlist) in
-  let base_mty = interp_modtype env mty in
+
+  let _ = Global.start_modtype id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
+  let base_mty = interp_modtype (Global.env()) mty in
   let entry = 
     List.fold_right 
       (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
@@ -730,27 +726,25 @@ let rec get_module_substobjs env = function
 
 
 let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
-
   let fs = Summary.freeze_summaries () in
-  let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
-  in
-  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  let _ = Global.start_module id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
   let mty_entry_o, mty_sub_o = match mty_o with
       None -> None, None
     | (Some (mty, true)) -> 
 	Some (List.fold_right 
 		(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
 		arg_entries 
-		(interp_modtype env mty)), 
+		(interp_modtype (Global.env()) mty)), 
 	None
     | (Some (mty, false)) -> 
 	None, 
 	Some (List.fold_right 
 		(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
 		arg_entries 
-		(interp_modtype env mty))
+		(interp_modtype (Global.env()) mty))
   in
   let mexpr_entry_o = match mexpr_o with
       None -> None
@@ -758,12 +752,13 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 	Some (List.fold_right 
 		(fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
 		arg_entries
-		(interp_modexpr env mexpr))
+		(interp_modexpr (Global.env()) mexpr))
   in
   let entry = 
     {mod_entry_type = mty_entry_o;	    
      mod_entry_expr = mexpr_entry_o }
   in
+  let env = Global.env() in
   let substobjs =
     match entry with
       | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
diff --git a/library/global.ml b/library/global.ml
index b4d3a7ff..863d26b7 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: global.ml 8723 2006-04-16 15:51:02Z herbelin $ *)
 
 open Util
 open Names
@@ -73,22 +73,27 @@ let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let start_module id params mtyo =
+let start_module id =
   let l = label_of_id id in
-  let mp,newenv = start_module l params mtyo !global_env in
+  let mp,newenv = start_module l !global_env in
     global_env := newenv;
     mp
-  
-let end_module id =
+
+let end_module id mtyo =
   let l = label_of_id id in
-  let mp,newenv = end_module l !global_env in
+  let mp,newenv = end_module l mtyo !global_env in
     global_env := newenv;
     mp
 
 
-let start_modtype id params = 
+let add_module_parameter mbid mte =
+  let newenv = add_module_parameter mbid mte !global_env in
+    global_env := newenv
+
+
+let start_modtype id =
   let l = label_of_id id in
-  let mp,newenv = start_modtype l params !global_env in
+  let mp,newenv = start_modtype l !global_env in
     global_env := newenv;
     mp
 
diff --git a/library/global.mli b/library/global.mli
index 278b9e65..96965465 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*)
+(*i $Id: global.mli 8723 2006-04-16 15:51:02Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -63,20 +63,13 @@ val set_engagement : engagement -> unit
 (* [start_*] functions return the [module_path] valid for components
    of the started module / module type *)
 
-val start_module : 
-  identifier -> (mod_bound_id * module_type_entry) list 
-    -> module_type_entry option 
-      -> module_path
+val start_module : identifier -> module_path
+val end_module : identifier -> module_type_entry option -> module_path
 
-val end_module :
-  identifier -> module_path
+val add_module_parameter : mod_bound_id -> module_type_entry -> unit
 
-val start_modtype :
-  identifier -> (mod_bound_id * module_type_entry) list
-    -> module_path
-
-val end_modtype :
-  identifier -> kernel_name
+val start_modtype : identifier -> module_path
+val end_modtype : identifier -> kernel_name
 
 
 (* Queries *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 08ae2aa5..68fc046c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
+(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Util
 open Names
@@ -282,14 +282,15 @@ let compute_mib_implicits kn =
   let ar =
     Array.to_list
       (Array.map  (* No need to lift, arities contain no de Bruijn *)
-        (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity))
+        (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip)))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)),
+    let ar = type_of_inductive (mib,mip) in
+    ((IndRef ind,auto_implicits env ar),
      Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
-       mip.mind_user_lc)
+       mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
 
diff --git a/library/lib.ml b/library/lib.ml
index ee553cad..ba6b9c79 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 7710 2005-12-23 10:16:42Z herbelin $ *)
+(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *)
 
 open Pp
 open Util
@@ -460,7 +460,7 @@ let open_section id =
 
 let discharge_item = function
   | ((sp,_ as oname),Leaf lobj) ->
-      option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+      option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
   | _ ->
       None
 
@@ -624,12 +624,30 @@ let reset_initial () =
 
 (* Misc *)
 
+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
+
+let rec dp_of_mp modp =
+  match modp with
+    | MPfile dp -> dp
+    | MPbound _ | MPself _ -> library_dp ()
+    | MPdot (mp,_) -> dp_of_mp mp
+
 let library_part ref =
+  match ref with 
+    | VarRef id -> library_dp ()
+    | _ -> dp_of_mp (mp_of_global ref)
+
+let remove_section_part ref =
   let sp = Nametab.sp_of_global ref in
   let dir,_ = repr_path sp in
   match ref with
   | VarRef id -> 
-      anomaly "library_part not supported on local variables"
+      anomaly "remove_section_part not supported on local variables"
   | _ ->
       if is_dirpath_prefix_of dir (cwd ()) then
         (* Not yet (fully) discharged *)
diff --git a/library/lib.mli b/library/lib.mli
index 22b6b6d8..e33c3aca 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
+(*i $Id: lib.mli 8852 2006-05-23 17:52:43Z notin $ i*)
 
 (*i*)
 open Util
@@ -122,7 +122,8 @@ val end_compilation : dir_path -> object_prefix * library_segment
 val library_dp : unit -> dir_path
 
 (* Extract the library part of a name even if in a section *)
-val library_part : global_reference -> dir_path
+val library_part :  global_reference -> dir_path
+val remove_section_part : global_reference -> dir_path
 
 (*s Sections *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 536a382d..48a7565e 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 7052 2005-05-20 15:54:50Z herbelin $ i*)
+(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*)
 
 open Pp
 open Util
@@ -78,6 +78,14 @@ let dirpath_prefix p = match repr_dirpath p with
 let is_dirpath_prefix_of d1 d2 =
   list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
 
+let chop_dirpath n d =
+  let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in
+    make_dirpath (List.rev d1), make_dirpath (List.rev d2)
+
+let drop_dirpath_prefix d1 d2 =
+  let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
+    make_dirpath (List.rev d)
+
 (* To know how qualified a name should be to be understood in the current env*)
 let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 06595e81..ab2185a6 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 7052 2005-05-20 15:54:50Z herbelin $ i*)
+(*i $Id: libnames.mli 8768 2006-04-28 14:25:31Z notin $ i*)
 
 (*i*)
 open Pp
@@ -53,6 +53,8 @@ val split_dirpath : dir_path -> dir_path * identifier
 val extend_dirpath : dir_path -> module_ident -> dir_path
 val add_dirpath_prefix : module_ident -> dir_path -> dir_path
 
+val chop_dirpath : int -> dir_path -> dir_path * dir_path
+val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
 val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 708c19b1..7f383a3b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
+(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Util
 open Names
@@ -109,12 +109,12 @@ let declare_object odecl =
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
   and discharge (oname,lobj) = 
     if Dyn.tag lobj = na then 
-      option_app infun (odecl.discharge_function (oname,outfun lobj))
+      option_map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
-      option_app infun (odecl.export_function (outfun lobj))
+      option_map infun (odecl.export_function (outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the exportfun"
 
diff --git a/library/library.ml b/library/library.ml
index 760b6f07..cfd88ca0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *)
 
 open Pp
 open Util
@@ -57,7 +57,6 @@ let canonical_path_name p =
     (* 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
   match list_filter2 (fun p d -> p = phys_dir) !load_paths with
@@ -65,38 +64,44 @@ let find_logical_path phys_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 lp = get_load_paths () in
+  let check_p = fun p -> (String.compare dir p) == 0 in
+    List.exists check_p lp 
+
 let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
   let phys_path = canonical_path_name phys_path in
-  match list_filter2 (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
-         && coq_path = Nameops.default_root_prefix)
-      then
-	begin
-          (* Assume the user is concerned by library naming *)
-	  if dir <> Nameops.default_root_prefix then
-	    (Options.if_verbose warning (phys_path^" was previously bound to "
-	    ^(string_of_dirpath dir)
-	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
-             flush_all ());
-	  remove_load_path phys_path;
-	  load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
-	end
-  | _,[] ->
-      load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-  | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+    match list_filter2 (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
+		&& coq_path = Nameops.default_root_prefix)
+	  then
+	    begin
+              (* Assume the user is concerned by library naming *)
+	      if dir <> Nameops.default_root_prefix then
+		(Options.if_verbose warning (phys_path^" was previously bound to "
+					     ^(string_of_dirpath dir)
+					     ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
+		 flush_all ());
+	      remove_load_path phys_path;
+	      load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+	    end
+      | _,[] ->
+	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+      | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
 let load_paths_of_dir_path dir =
   fst (list_filter2 (fun p d -> d = dir) !load_paths)
-
+    
 let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 (************************************************************************)
diff --git a/library/library.mli b/library/library.mli
index f7620682..27ace544 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 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id: library.mli 8877 2006-05-30 16:37:04Z notin $ i*)
 
 (*i*)
 open Util
@@ -64,6 +64,7 @@ val get_full_load_paths : unit -> (System.physical_path * dir_path) list
 val add_load_path : System.physical_path * dir_path -> unit
 val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
+val is_in_load_paths : System.physical_path -> bool
 val load_paths_of_dir_path : dir_path -> System.physical_path list
 
 (*s Locate a library in the load paths *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 6db5f75d..1c6a7d56 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 6205 2004-10-12 10:13:15Z herbelin $ *)
+(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *)
 
 open Pp
 open Util
@@ -138,7 +138,7 @@ let next_ident_away_from id avoid =
 
 let out_name = function
   | Name id -> id
-  | Anonymous -> anomaly "out_name: expects a defined name"
+  | Anonymous -> failwith "out_name: expects a defined name"
 
 let name_fold f na a =
   match na with