diff options
| author | Enrico Tassi | 2014-10-08 17:28:18 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-13 18:13:20 +0200 |
| commit | 7cfcaa57a68ea9abde9e2558ceef86589aa26d6d (patch) | |
| tree | 4a6b0795b7a4408b0651d34146329495b423ff29 /toplevel | |
| parent | e3a0a4d58b74d2113485ceabe4235567fda962c8 (diff) | |
STM: primitives to snapshot a .vi while in interactive mode
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 dcce581994..b56b515dc6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -333,8 +333,8 @@ let compile verbosely f = let _ = load_vernac verbosely long_f_dot_v in Stm.finish (); check_pending_proofs (); - Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v - (Global.opaque_tables ()) + Stm.snapshot_vi ldir long_f_dot_v; + Stm.reset_task_queue () | Vi2Vo -> let open Filename in let open Library in |