aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-13 23:57:43 +0100
committerMaxime Dénès2017-12-13 23:57:43 +0100
commit671c4dbd064884a042d8f2bea5186ab5c7eaaeec (patch)
tree5b96358dbceed10a46fa42ecde293c0fe8d6ce7a /lib/flags.ml
parentb1aaedb9e728702cccdb1bd126a714d9e075d14c (diff)
parent50159f9c1748ccf1d66341d171081a998d116d2f (diff)
Merge PR #1108: [stm] Reorganize flags
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml28
1 files changed, 1 insertions, 27 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index ddc8f84825..b43d5f74d2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -35,36 +35,10 @@ let record_aux_file = ref false
let test_mode = ref false
-type async_proofs = APoff | APonLazy | APon
-let async_proofs_mode = ref APoff
-type cache = Force
-let async_proofs_cache = ref None
-let async_proofs_n_workers = ref 1
-let async_proofs_n_tacworkers = ref 2
-let async_proofs_private_flags = ref None
-let async_proofs_full = ref false
-let async_proofs_never_reopen_branch = ref false
-let async_proofs_flags_for_workers = ref []
let async_proofs_worker_id = ref "master"
-type priority = Low | High
-let async_proofs_worker_priority = ref Low
-let string_of_priority = function Low -> "low" | High -> "high"
-let priority_of_string = function
- | "low" -> Low
- | "high" -> High
- | _ -> raise (Invalid_argument "priority_of_string")
-type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
-let async_proofs_cmd_error_resilience = ref true
-
-let async_proofs_is_worker () =
- !async_proofs_worker_id <> "master"
-let async_proofs_is_master () =
- !async_proofs_mode = APon && !async_proofs_worker_id = "master"
-let async_proofs_delegation_threshold = ref 0.03
+let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
let debug = ref false
-let stm_debug = ref false
let in_debugger = ref false
let in_toplevel = ref false