From ed18f926e4695acc730218925ca156abe56ba5fc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 13 Feb 2018 18:26:00 +0100
Subject: [toplevel] Make toplevel state into a record.

We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
---
 stm/proofworkertop.ml | 2 +-
 stm/queryworkertop.ml | 2 +-
 stm/stm.ml            | 3 +--
 stm/tacworkertop.ml   | 2 +-
 4 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'stm')

diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index def60d1b99..81637f143d 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 928a6bfb05..7862f2f447 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 6c956e1342..92587b8ea5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2106,8 +2106,7 @@ and Reach : sig
 end = struct (* {{{ *)
 
 let async_policy () =
-  let open Flags in
-  if is_universe_polymorphism () then false
+  if Flags.is_universe_polymorphism () then false
   else if VCS.is_interactive () = `Yes then
     (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index f202fc7c55..22b45a9be8 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
-- 
cgit v1.2.3