diff options
| author | Maxime Dénès | 2018-02-19 11:11:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-19 11:11:50 +0100 |
| commit | 073b92396a68be30f77c80960a58ca562bb01f49 (patch) | |
| tree | d2ad366f28624196ebfe9c1eadf595dcb490fcdc /stm | |
| parent | c047ecce6e4dba33df69a53a9e168999676c65db (diff) | |
| parent | ed18f926e4695acc730218925ca156abe56ba5fc (diff) | |
Merge PR #6753: [toplevel] Make toplevel state into a record.
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 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 ()) |