diff options
| author | Maxime Dénès | 2018-11-23 13:12:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-27 15:09:19 +0100 |
| commit | 3bffd4f4f4a9ef400781aa7a4f90a986891bb0c1 (patch) | |
| tree | d54a59e4451ede662f70d1efb5ca2bf987d41f31 /toplevel | |
| parent | 0a699c7c932352f38c14f1bdf33ee7955241c1d8 (diff) | |
Remove -async-proofs-full flag
The semantics of this flag was not clear, it had several rather
orthogonal effects. Also, it should probably have been another value of
`-async-proofs-mode`, rather than a separate flag, as its combination
with e.g. `-async-proofs-mode off` is unclear.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 2f84eb9851..b98535b201 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -543,10 +543,6 @@ let parse_args arglist : coq_cmdopts * string list = (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - { oval with stm_flags = { oval.stm_flags with - Stm.AsyncOpts.async_proofs_full = true; - }} |"-async-proofs-never-reopen-branch" -> { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true |