aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-02 16:01:46 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-02 16:01:46 +0200
commit16c88c9be5c37ee2e4fe04f7342365964031e7dd (patch)
tree7b5c07362dad323acae516718b9cebe94bd639af /checker
parenta3d7630d74b720b771e880dcf0fcad05de553a6e (diff)
parent88abc50ece70405d71777d5350ca2fa70c1ff437 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml18
1 files changed, 4 insertions, 14 deletions
diff --git a/checker/check.ml b/checker/check.ml
index c835cec82..2bc470aea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -271,20 +271,10 @@ let try_locate_qualified_library qid =
| LibNotFound -> error_lib_not_found qid
(************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
+(*s Low-level interning of libraries from files *)
-(*s Loading from disk to cache (preparation phase) *)
-
-let raw_intern_library =
- snd (System.raw_extern_intern Coq_config.vo_magic_number)
-
-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.")
+let raw_intern_library f =
+ System.raw_intern_state Coq_config.vo_magic_number f
(************************************************************************)
(* Internalise libraries *)
@@ -312,7 +302,7 @@ let intern_from_file (dir, f) =
Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
let (sd,md,table,opaque_csts,digest) =
try
- let ch = with_magic_number_check raw_intern_library f in
+ let ch = System.with_magic_number_check raw_intern_library f in
let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in