diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-05 21:21:43 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 14:04:33 -0400 |
| commit | 845dd3dd17b880999a956839c0d84d46de9e27b8 (patch) | |
| tree | 10897262434b5bfa6a78bceaac8cab33ca7acd1b /toplevel | |
| parent | e4d66a03148243f7611f4d7c164e775877184e03 (diff) | |
STM: each proof block can be enabled separately
By default we enable only {} and par: that are detectable in
a complete way.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c52830ea7..e1f5a70c2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -379,6 +379,11 @@ let get_host_port opt s = prerr_endline ("Error: host:port or stdfds expected after option "^opt); exit 1 +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (String.split ',' s) + let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) let vio_tasks = ref [] @@ -493,7 +498,7 @@ let parse_args arglist = |"-async-proofs-private-flags" -> Flags.async_proofs_private_flags := Some (next ()); |"-async-proofs-tactic-error-resilience" -> - Flags.async_proofs_tac_error_resilience := get_bool opt (next ()) + Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) |"-async-proofs-command-error-resilience" -> Flags.async_proofs_cmd_error_resilience := get_bool opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |