From 95e723892c336808aad0926c675f3e0ac8ba7d99 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 14:10:22 +0100
Subject: Remove global output_native_objects flag.

---
 stm/stm.ml  | 5 +++--
 stm/stm.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 0165b3c029..5b13fc6a37 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2885,11 +2885,12 @@ let handle_failure (e, info) vcs =
   VCS.print ();
   Exninfo.iraise (e, info)
 
-let snapshot_vio ~doc ldir long_f_dot_vo =
+let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
   let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
+  Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
+    ldir long_f_dot_vo
     (Global.opaque_tables ());
   doc
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 821ab59a43..91651e3534 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -156,7 +156,7 @@ val join : doc:doc -> doc
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
      of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
+val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)
-- 
cgit v1.2.3