diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-13 18:26:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-15 11:37:51 +0100 |
| commit | ed18f926e4695acc730218925ca156abe56ba5fc (patch) | |
| tree | 390d1fef8613afbfe4c5e2de3209e06f48f59122 /stm | |
| parent | 4bc9529ece085441121678a07e4b269c7633471c (diff) | |
[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.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 3 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 2 |
4 files changed, 4 insertions, 5 deletions
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index def60d1b9..81637f143 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 928a6bfb0..7862f2f44 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 6c956e134..92587b8ea 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 f202fc7c5..22b45a9be 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 ()) |