diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-17 10:21:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-24 00:13:17 +0200 |
| commit | e2e88741120332f9e97459852d7361e2d8939881 (patch) | |
| tree | 9674a8785e31974fb73b96b840014d86d5e14b1b /toplevel | |
| parent | a2fa3dd1ec96cd70c817ff375d7b857924bb9825 (diff) | |
Splitting the library representation on disk in two.
The first part only contains the summary of the library, while the second
one contains the effective content of it.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7d84ecf6c..bc8aa2fff 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -344,10 +344,10 @@ let compile verbosely f = let open Library in Dumpglob.noglob (); let f = if check_suffix f ".vio" then chop_extension f else f in - let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in + let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in Stm.set_compilation_hints lfdv; let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in - Library.save_library_raw lfdv lib univs proofs + Library.save_library_raw lfdv sum lib univs proofs let compile v f = ignore(CoqworkmgrApi.get 1); |