diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4ea9c2236..11cb726c7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -348,6 +348,6 @@ let compile verbosely f = let f = if check_suffix f ".vi" then chop_extension f else f in let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv); - Stm.finish_tasks lfdv univs disch proofs tasks; + let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv lib univs proofs |