Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

5 files changed, 29 insertions, 30 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 93021384..cfada00c 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 12204 2009-06-22 16:06:49Z soubiran $ i*)
+(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -851,8 +851,7 @@ let classify_import (_,(export,_ as obj)) =
   if export then Substitute obj else Dispose
 
 let subst_import (_,subst,(export,mp as obj)) =
-  let subst' = remove_alias subst in
-  let mp' = subst_mp subst' mp in
+  let mp' = subst_mp subst mp in
     if mp'==mp then obj else
       (export,mp')
 	
diff --git a/library/goptions.ml b/library/goptions.ml
index a9b33235..8625ee52 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id: goptions.ml 13196 2010-06-25 18:01:50Z herbelin $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -297,10 +297,11 @@ let set_int_option_value = set_option_value
   (fun v -> function 
      | (IntValue _) -> IntValue v
      | _ -> bad_type_error ())
-let set_bool_option_value = set_option_value
-  (fun v -> function 
+let set_bool_option_value key v =
+  try set_option_value (fun v -> function
      | (BoolValue _) -> BoolValue v
-     | _ -> bad_type_error ())
+     | _ -> bad_type_error ()) key v
+  with UserError (_,s) -> Flags.if_verbose msg_warning s
 let set_string_option_value = set_option_value
  (fun v -> function 
     | (StringValue _) -> StringValue v
diff --git a/library/lib.ml b/library/lib.ml
index 4a124cec..f0ec488b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: lib.ml 12496 2009-11-11 13:37:57Z herbelin $ *)
 
 open Pp
 open Util
@@ -171,9 +171,8 @@ let find_split_p p =
 
 let split_lib_gen test = 
   let rec collect after equal = function
-    | hd::strict_before as before ->
-      	if test hd then collect after (hd::equal) strict_before else after,equal,before
-    | [] as before -> after,equal,before
+    | hd::before when test hd -> collect after (hd::equal) before
+    | before -> after,equal,before
   in
   let rec findeq after = function
     | hd :: before ->
@@ -194,7 +193,14 @@ let split_lib_gen test =
       | None -> error "no such entry"
       | Some r -> r
 
-let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
+let split_lib sp = split_lib_gen (fun x -> fst x = sp)
+
+let split_lib_at_opening sp =
+  split_lib_gen (function
+    | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) ->
+	x = sp
+    | _ ->
+	false)
 
 (* Adding operations. *)
 
@@ -299,7 +305,7 @@ let end_module id =
     with Not_found ->
       error "no opened modules"
   in
-  let (after,modopening,before) = split_lib oname in
+  let (after,modopening,before) = split_lib_at_opening oname in
   lib_stk := before;
   add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
   let prefix = !path_prefix in
@@ -344,7 +350,7 @@ let end_modtype id =
     with Not_found ->
       error "no opened module types"
   in
-  let (after,modtypeopening,before) = split_lib sp in
+  let (after,modtypeopening,before) = split_lib_at_opening sp in
   lib_stk := before;
   add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
   let dir = !path_prefix in
@@ -407,7 +413,7 @@ let end_compilation dir =
 	    ("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
+  let (after,_,before) = split_lib_at_opening oname in
     comp_name := None;
     !path_prefix,after
 
@@ -587,7 +593,7 @@ let close_section id =
     with Not_found ->
       error "No opened section."
   in
-  let (secdecls,secopening,before) = split_lib oname in
+  let (secdecls,secopening,before) = split_lib_at_opening oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
@@ -640,7 +646,7 @@ let reset_to_gen test =
   let (_,_,before) = split_lib_gen test in
   set_lib_stk before
 
-let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
+let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
 let reset_to_state sp =
   let (_,eq,before) = split_lib sp in
@@ -667,7 +673,7 @@ let delete_gen test =
  in
   set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
 
-let delete sp = delete_gen (fun x -> (fst x) = sp)
+let delete sp = delete_gen (fun x -> fst x = sp)
 
 let reset_name (loc,id) =
   let (sp,_) = 
diff --git a/library/library.ml b/library/library.ml
index 0e1342f0..2c6d02ae 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -328,14 +328,6 @@ let (in_import, out_import) =
 let (raw_extern_library, raw_intern_library) =
   System.raw_extern_intern Coq_config.vo_magic_number ".vo"
 
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
-
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
@@ -414,7 +406,7 @@ let mk_library md digest = {
   library_digest = digest }
 
 let intern_from_file f =
-  let ch = with_magic_number_check raw_intern_library f in
+  let ch = System.with_magic_number_check raw_intern_library f in
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
   close_in ch;
diff --git a/library/states.ml b/library/states.ml
index c81f9614..3a4be1ca 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
+(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open System
 
@@ -24,7 +24,8 @@ let (extern_state,intern_state) =
     extern_intern Coq_config.state_magic_number ".coq" in
   (fun s -> raw_extern s (freeze())),
   (fun s ->
-    unfreeze (raw_intern (Library.get_load_paths ()) s);
+    unfreeze
+      (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
     Library.overwrite_library_filenames s)
 
 (* Rollback. *)