Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

4 files changed, 14 insertions, 13 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 80da9e73..db7b8915 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -990,9 +990,9 @@ let declare_include_ interp_struct me_asts =
 let protect_summaries f =
   let fs = Summary.freeze_summaries () in
   try f fs
-  with e ->
+  with reraise ->
     (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
+    Summary.unfreeze_summaries fs; raise reraise
 
 let declare_include interp_struct me_asts =
   protect_summaries
diff --git a/library/heads.ml b/library/heads.ml
index b860dc2a..c33ea9b1 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -88,7 +88,7 @@ let kind_of_head env t =
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
   | Cast (c,_,_) -> aux k l c b
   | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
-  | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b
+  | Lambda (_,_,c) -> aux k (List.tl l) (subst1 (List.hd l) c) b
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
diff --git a/library/impargs.ml b/library/impargs.ml
index c79edb99..930b8f09 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -74,9 +74,9 @@ let with_implicits flags f x =
     let rslt = f x in
     implicit_args := oflags;
     rslt
-  with e -> begin
+  with reraise -> begin
     implicit_args := oflags;
-    raise e
+    raise reraise
   end
 
 let set_maximality imps b =
diff --git a/library/library.ml b/library/library.ml
index 30e7b675..c857fc86 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -368,14 +368,14 @@ let explain_locate_library_error qid = function
 let try_locate_absolute_library dir =
   try
     locate_absolute_library dir
-  with e ->
+  with e when Errors.noncritical e ->
     explain_locate_library_error (qualid_of_dirpath dir) e
 
 let try_locate_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
     dir,f
-  with e ->
+  with e when Errors.noncritical e ->
     explain_locate_library_error qid e
 
 
@@ -398,20 +398,20 @@ let fetch_opaque_table (f,pos,digest) =
   try
     let ch = System.with_magic_number_check raw_intern_library f in
     seek_in ch pos;
-    if System.marshal_in ch <> digest then failwith "File changed!";
-    let table = (System.marshal_in ch : LightenLibrary.table) in
+    if System.marshal_in f ch <> digest then failwith "File changed!";
+    let table = (System.marshal_in f ch : LightenLibrary.table) in
     close_in ch;
     table
-  with _ ->
+  with e when Errors.noncritical e ->
     error
       ("The file "^f^" is inaccessible or has changed,\n" ^
        "cannot load some opaque constant bodies in it.\n")
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let lmd = System.marshal_in ch in
+  let lmd = System.marshal_in f ch in
   let pos = pos_in ch in
-  let digest = System.marshal_in ch in
+  let digest = System.marshal_in f ch in
   let table = lazy (fetch_opaque_table (f,pos,digest)) in
   register_library_filename lmd.md_name f;
   let library = mk_library lmd table digest in
@@ -655,7 +655,8 @@ let save_library_to dir f =
     System.marshal_out ch di;
     System.marshal_out ch table;
     close_out ch
-  with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
+  with reraise ->
+    warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise
 
 (************************************************************************)
 (*s Display the memory use of a library. *)