diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 15:31:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 15:31:10 +0200 |
| commit | 2c9854dec504140b6f813af294aa83b14b5af3e5 (patch) | |
| tree | c7ee834f9b433c51a4028d9818bb8327787108b5 | |
| parent | 1839b83248ea380f1cecc165d5d9401f9e450784 (diff) | |
| parent | 6334ab72d55cb93a877933bd3f56a90d859d518d (diff) | |
Merge PR #12188: Do not delay the loading of the library_disk field when requiring libraries
Reviewed-by: ejgallego
| -rw-r--r-- | vernac/library.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index 35b2a18871..afadbd704d 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -92,7 +92,7 @@ type summary_disk = { type library_t = { library_name : compilation_unit_name; - library_data : library_disk delayed; + library_data : library_disk; library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_digests : Safe_typing.vodigest; library_extra_univs : Univ.ContextSet.t; @@ -243,7 +243,7 @@ let mk_summary m = { let intern_from_file f = let ch = raw_intern_library f in let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in - let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch ~segment:"library" in + let ((lmd : seg_lib), digest_lmd) = ObjFile.marshal_in_segment ch ~segment:"library" in let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; @@ -317,7 +317,7 @@ let native_name_from_filename f = *) let register_library m = - let l = fetch_delayed m.library_data in + let l = m.library_data in Declaremods.register_library m.library_name l.md_compiled |