diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 6 | ||||
| -rw-r--r-- | library/impargs.ml | 6 | ||||
| -rw-r--r-- | library/library.ml | 8 |
3 files changed, 10 insertions, 10 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index c30b2099f9..366fb77a01 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1004,11 +1004,11 @@ 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 *) - let e = Errors.push e in + let reraise = Errors.push reraise in let () = Summary.unfreeze_summaries fs in - raise e + raise reraise let declare_include interp_struct me_asts = protect_summaries diff --git a/library/impargs.ml b/library/impargs.ml index 217169a610..56dca8e3f3 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -75,10 +75,10 @@ let with_implicits flags f x = let rslt = f x in implicit_args := oflags; rslt - with e -> - let e = Errors.push e in + with reraise -> + let reraise = Errors.push reraise in let () = implicit_args := oflags in - raise e + raise reraise let set_maximality imps b = (* Force maximal insertion on ending implicits (compatibility) *) diff --git a/library/library.ml b/library/library.ml index 0243968b9c..a5f93c02c1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -406,7 +406,7 @@ let fetch_opaque_table (f,pos,digest) = 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") @@ -667,12 +667,12 @@ let save_library_to dir f = | 0 -> () | _ -> anomaly (Pp.str "Library compilation failure") end - with e -> - let e = Errors.push e in + with reraise -> + let reraise = Errors.push reraise in let () = msg_warning (str ("Removed file "^f')) in let () = close_out ch in let () = Sys.remove f' in - raise e + raise reraise (************************************************************************) (*s Display the memory use of a library. *) |