Imported Upstream version 8.0pl2upstream/8.0pl2

9 files changed, 46 insertions, 28 deletions

diff --git a/library/declaremods.mli b/library/declaremods.mli
index f229da1e..f896310a 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declaremods.mli,v 1.8.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -85,7 +85,7 @@ val end_library :
 
 
 (* [really_import_module mp] opens the module [mp] (in a Caml sense).
-   It modifies Nametab and performs the "open_object" function for
+   It modifies Nametab and performs the [open_object] function for
    every object of the module. *)
 
 val really_import_module : module_path -> unit
@@ -109,7 +109,7 @@ val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
 
 val debug_print_modtab : unit -> Pp.std_ppcmds
 
-(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*)
+(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*)
 
 (* For translator *)
 val process_module_bindings : module_ident list ->
diff --git a/library/lib.ml b/library/lib.ml
index b9da6dea..a9f864ef 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml,v 1.63.2.2 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: lib.ml,v 1.63.2.3 2004/11/22 14:21:23 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -564,3 +564,15 @@ let library_part ref =
       else
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
+
+
+let rec file_of_mp = function
+  | MPfile dir -> Some dir
+  | MPself _ -> Some (library_dp ())
+  | MPbound _ -> None
+  | MPdot (mp,_) -> file_of_mp mp
+
+let file_part = function
+  | VarRef id -> anomaly "TODO";
+  | ConstRef kn | ConstructRef ((kn,_),_) | IndRef (kn,_) -> 
+      file_of_mp (modpath kn)
diff --git a/library/lib.mli b/library/lib.mli
index 8981754e..aa874470 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,v 1.41.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: lib.mli,v 1.41.2.3 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -59,7 +59,7 @@ val add_leaf : identifier -> obj -> object_name
 val add_absolutely_named_leaf : object_name -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 
-(* this operation adds all objects with the same name and calls load_object 
+(* 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
 
@@ -107,7 +107,7 @@ val start_modtype :
   module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_modtype : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
-(* Lib.add_frozen_state must be called after each of the above functions *)
+(* [Lib.add_frozen_state] must be called after each of the above functions *)
 
 (*s Compilation units *)
 
@@ -121,6 +121,9 @@ 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
 
+(* Extract the library part of a name if not in a functor *)
+val file_part : global_reference -> dir_path option
+
 (*s Sections *)
 
 val open_section : identifier -> object_prefix
diff --git a/library/libnames.mli b/library/libnames.mli
index 6f05333c..a6055428 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,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: libnames.mli,v 1.8.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Pp
@@ -111,8 +111,8 @@ val qualid_of_dirpath : dir_path -> qualid
 
 val make_short_qualid : identifier -> qualid
 
-(* Both names are passed to objects: a "semantic" kernel_name, which
-   can be substituted and a "syntactic" section_path which can be printed
+(* Both names are passed to objects: a "semantic" [kernel_name], which
+   can be substituted and a "syntactic" [section_path] which can be printed
 *)
 
 type object_name = section_path * kernel_name
@@ -121,7 +121,7 @@ type object_prefix = dir_path * (module_path * dir_path)
 
 val make_oname : object_prefix -> identifier -> object_name
 
-(* to this type are mapped dir_path's in the nametab *)
+(* to this type are mapped [dir_path]'s in the nametab *)
 type global_dir_reference = 
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
diff --git a/library/libobject.mli b/library/libobject.mli
index 8a3811e1..b9070f5d 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libobject.mli,v 1.9.8.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: libobject.mli,v 1.9.8.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -39,7 +39,7 @@ open Libnames
      Keep      - the object is not substitutive, but survives module 
                  closing
      Anticipate - this is for objects which have to be explicitely 
-                 managed by the end_module function (like Require 
+                 managed by the [end_module] function (like Require 
                  and Read markers)
 
      The classification function is also an occasion for a cleanup
diff --git a/library/library.ml b/library/library.ml
index 0477a8f3..cbc8874a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml,v 1.79.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: library.ml,v 1.79.2.2 2004/11/17 14:01:26 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -169,8 +169,10 @@ let _ =
       Summary.survive_section = false }
 
 let find_library s =
-  try
-    CompilingLibraryMap.find s !libraries_table
+  CompilingLibraryMap.find s !libraries_table
+
+let try_find_library s =
+  try find_library s
   with Not_found ->
     error ("Unknown library " ^ (string_of_dirpath s))
 
@@ -250,7 +252,7 @@ let open_libraries export modl =
       (fun l m ->
          let subimport =
            List.fold_left
-             (fun l m -> remember_last_of_each l (find_library m))
+             (fun l m -> remember_last_of_each l (try_find_library m))
              l m.library_imports
          in remember_last_of_each subimport m)
       [] modl in
@@ -261,7 +263,7 @@ let open_libraries export modl =
 (* import and export  -  synchronous operations*)
 
 let cache_import (_,(dir,export)) = 
-  open_libraries export [find_library dir]
+  open_libraries export [try_find_library dir]
 
 let open_import i (_,(dir,_) as obj) =
   if i=1 then
@@ -698,7 +700,7 @@ let check_required_library d =
 open Printf
 
 let mem s =
-  let m = find_library s in
+  let m = try_find_library s in
   h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
 		 (size_kb m) (size_kb m.library_compiled) 
 		 (size_kb m.library_objects)))
diff --git a/library/nameops.ml b/library/nameops.ml
index ea40aae5..35b707a7 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml,v 1.21.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: nameops.ml,v 1.21.2.2 2004/10/12 10:12:31 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -29,8 +29,8 @@ let cut_ident skip_quote s =
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
     if n = 0 then 
-      error
-	("The string " ^ s ^ " is not an identifier: it contains only digits or _")
+      (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
+      slen
     else 
       let c = Char.code (String.get s (n-1)) in
       if c = code_of_0 && n <> slen then 
diff --git a/library/nameops.mli b/library/nameops.mli
index 4b7cecda..71dbf040 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.mli,v 1.12.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(*i $Id: nameops.mli,v 1.12.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Names
 
@@ -18,7 +18,7 @@ val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
 val atompart_of_id : identifier -> string  (* remove trailing digits *)
-val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *)
+val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *)
 
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier
diff --git a/library/nametab.mli b/library/nametab.mli
index 3a0bd670..08a9d1bb 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nametab.mli,v 1.43.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: nametab.mli,v 1.43.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -33,13 +33,14 @@ open Libnames
 
    \item [locate : qualid -> object_reference]
 
-   Finds the object referred to by [qualid] or raises Not_found 
+   Finds the object referred to by [qualid] or raises [Not_found]
    
-   \item [name_of] : object_reference -> user_name
+   \item [name_of : object_reference -> user_name]
 
    The [user_name] can be for example the shortest non ambiguous [qualid] or 
    the [full_user_name] or [identifier]. Such a function can also have a 
    local context argument. 
+   \end{itemize}
 *)
    
   
@@ -155,7 +156,7 @@ val id_of_global : global_reference -> identifier
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
 
 
-(* The [shortest_qualid] functions given an object with user_name
+(* The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)