Imported Upstream version 8.0pl3upstream/8.0pl3

8 files changed, 35 insertions, 58 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 8b9dfeda..cfa8890a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml,v 1.128.2.1 2004/07/16 19:30:34 herbelin Exp $ *)
+(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *)
 
 open Pp
 open Util
@@ -271,6 +271,7 @@ let dummy_one_inductive_entry mie = {
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_inductive_entry m = {
+  mind_entry_record = false;
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b968a432..2e8fb0a7 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,v 1.18.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*)
 
 open Pp
 open Util
@@ -502,17 +502,17 @@ let end_module id =
   let dir = fst oldprefix in
   let msid = msid_of_prefix oldprefix in
 
-  let substobjs = try
+  let substobjs, keep, special = try
     match res_o with
       | None -> 
-	  empty_subst, mbids, msid, substitute
+	  (empty_subst, mbids, msid, substitute), keep, special
       | Some (MTEident ln) ->
-	  abstract_substobjs mbids (KNmap.find ln (!modtypetab))
+	  abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], []
       | Some (MTEsig (msid,_)) ->
 	  todo "Anonymous signatures not supported";
-	  empty_subst, mbids, msid, []
+	  (empty_subst, mbids, msid, []), keep, special
       | Some (MTEwith _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs mty)
+	  abstract_substobjs mbids (get_modtype_substobjs mty), [], []
       | Some (MTEfunsig _) -> 
 	  anomaly "Funsig cannot be here..."
     with
diff --git a/library/global.ml b/library/global.ml
index bfa9335c..8694d7af 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml,v 1.43.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *)
 
 open Util
 open Names
@@ -25,6 +25,8 @@ let safe_env () = !global_env
 
 let env () = env_of_safe_env !global_env
 
+let env_is_empty () = is_empty !global_env
+
 let _ = 
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index 1da5965c..007986d1 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,v 1.40.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: global.mli,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*)
 
 (*i*)
 open Names
@@ -32,6 +32,8 @@ val env : unit -> Environ.env
 val universes : unit -> universes
 val named_context : unit -> Sign.named_context
 
+val env_is_empty : unit -> bool
+
 (*s Extending env with variables and local definitions *)
 val push_named_assum : (identifier * types) -> Univ.constraints
 val push_named_def   : (identifier * constr * types option) -> Univ.constraints
diff --git a/library/lib.ml b/library/lib.ml
index a9f864ef..c46634f4 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.3 2004/11/22 14:21:23 herbelin Exp $ *)
+(* $Id: lib.ml,v 1.63.2.4 2005/11/04 09:02:38 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -555,8 +555,7 @@ let library_part ref =
   let dir,_ = repr_path sp in
   match ref with
   | VarRef id -> 
-      anomaly "TODO";
-      extract_dirpath_prefix (sections_depth ()) (cwd ())
+      anomaly "library_part not supported on local variables"
   | _ ->
       if is_dirpath_prefix_of dir (cwd ()) then
         (* Not yet (fully) discharged *)
diff --git a/library/library.ml b/library/library.ml
index cbc8874a..aaed4545 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.2 2004/11/17 14:01:26 herbelin Exp $ *)
+(* $Id: library.ml,v 1.79.2.5 2006/01/10 17:06:23 barras Exp $ *)
 
 open Pp
 open Util
@@ -29,53 +29,26 @@ let load_path = ref ([],[] : System.physical_path list * logical_path list)
 
 let get_load_path () = fst !load_path
 
-(* 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_filter2 (fun p d -> p = phys_dir) !load_path with
   | _,[dir] -> dir
   | _,[] -> Nameops.default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let remove_path dir =
+  let dir = System.canonical_path_name dir in
   load_path := list_filter2 (fun p d -> p <> dir) !load_path
 
 let add_load_path_entry (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_filter2 (fun p d -> p = phys_path) !load_path 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
@@ -290,8 +263,8 @@ let (in_import, out_import) =
 (************************************************************************)
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
-let vo_magic_number8 = 08002 (* V8.0 final new syntax *)
+let vo_magic_number7 = 07993 (* V8.0pl3 final old syntax *)
+let vo_magic_number8 = 08003 (* V8.0pl3 final new syntax *)
 
 let (raw_extern_library7, raw_intern_library7) =
   System.raw_extern_intern vo_magic_number7 ".vo"
@@ -453,13 +426,8 @@ let rec_intern_by_filename_only id f =
     m.library_name
 
 let locate_qualified_library qid =
-  (* Look if loaded in current environment *)
-  try 
-    let dir = Nametab.full_name_module qid in
-    (LibLoaded, dir, library_full_filename dir)
-  with Not_found ->
-  (* Look if in loadpath *)
   try
+    (* Search library in loadpath *)
     let dir, base = repr_qualid qid in 
     let loadpath =
       if repr_dirpath dir = [] then get_load_path ()
@@ -470,7 +438,12 @@ let locate_qualified_library qid =
     if loadpath = [] then raise LibUnmappedDir;
     let name =  (string_of_id base)^".vo" in
     let path, file = System.where_in_path loadpath name in
-    (LibInPath, extend_dirpath (find_logical_path path) base, file)
+    let dir = extend_dirpath (find_logical_path path) base in
+    (* Look if loaded *)
+    try 
+      (LibLoaded, dir, library_full_filename dir)      
+    with Not_found ->
+      (LibInPath, dir, file)
   with Not_found -> raise LibNotFound
 
 let rec_intern_qualified_library (loc,qid) =
diff --git a/library/nametab.ml b/library/nametab.ml
index f009d867..4bd0cb3f 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nametab.ml,v 1.48.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: nametab.ml,v 1.48.2.2 2005/11/21 09:16:27 herbelin Exp $ *)
 
 open Util
 open Pp
@@ -472,9 +472,9 @@ let shortest_qualid_of_global ctx ref =
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
         SpTab.shortest_qualid ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef kn = 
+let shortest_qualid_of_syndef ctx kn = 
   let sp = sp_of_syntactic_definition kn in
-    SpTab.shortest_qualid Idset.empty sp !the_ccitab
+    SpTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_module mp = 
   let dir = MPmap.find mp !the_modrevtab in
diff --git a/library/nametab.mli b/library/nametab.mli
index 08a9d1bb..4cea1d40 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.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: nametab.mli,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -144,7 +144,7 @@ val full_name_module : qualid -> dir_path
 
 val sp_of_syntactic_definition : kernel_name -> section_path
 val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : kernel_name -> qualid
+val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid
 val shortest_qualid_of_tactic : ltac_constant -> qualid
 
 val dir_of_mp : module_path -> dir_path