diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738ca..ba19c7a63b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -47,6 +47,7 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let compilation_output_name = ref None let test_mode = ref false @@ -68,11 +69,15 @@ 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 [ "par" ; "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 debug = ref false let in_debugger = ref false @@ -220,6 +225,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode |