diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 18:54:06 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 18:54:06 +0200 |
| commit | e278d031a1d9a7bf3de463d3d415065299c99395 (patch) | |
| tree | ddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /library/library.ml | |
| parent | d7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff) | |
| parent | 3ce70f21a18cc19e720e8ac54b93652527881942 (diff) | |
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/library.ml b/library/library.ml index cead90700..12090183a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names @@ -64,7 +64,7 @@ let fetch_delayed del = let () = close_in ch in if not (String.equal digest digest') then raise (Faulty f); obj - with e when Errors.noncritical e -> raise (Faulty f) + with e when CErrors.noncritical e -> raise (Faulty f) end @@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab = except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> - if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.errorlabstrm "library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { @@ -756,8 +756,8 @@ let save_library_to ?todo dir f otab = if not (Nativelib.compile_library dir ast fn) then error "Could not compile the library to native code." with reraise -> - let reraise = Errors.push reraise in - let () = Feedback.msg_notice (str "Removed file " ++ str f') in + let reraise = CErrors.push reraise in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise |