diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 12:42:04 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 12:42:04 +0200 |
| commit | 33879a1d19fe0156a66c55be17b3ca94a0343fb9 (patch) | |
| tree | ff63a89f837b2f8c822eead3ccfd06ed998f3e05 /toplevel | |
| parent | ad3d0ce65ea4debacc98b50f58a96338c7bffc5d (diff) | |
| parent | d46e4bc63587c1b628cc80b3eac7a132a58d534d (diff) | |
Merge remote-tracking branch 'origin/pr/182' into trunk
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ceaaa112e..a488bb3e6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -370,6 +370,11 @@ let get_int opt n = with Failure _ -> prerr_endline ("Error: integer expected after option "^opt); exit 1 +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + let get_host_port opt s = match CString.split ':' s with | [host; portr; portw] -> @@ -501,6 +506,8 @@ let parse_args arglist = 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 ()) + |"-async-proofs-delegation-threshold" -> + Flags.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |