diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-02 16:01:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-02 16:01:46 +0200 |
| commit | 16c88c9be5c37ee2e4fe04f7342365964031e7dd (patch) | |
| tree | 7b5c07362dad323acae516718b9cebe94bd639af /checker | |
| parent | a3d7630d74b720b771e880dcf0fcad05de553a6e (diff) | |
| parent | 88abc50ece70405d71777d5350ca2fa70c1ff437 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 18 |
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 |