diff options
| -rw-r--r-- | stm/asyncTaskQueue.ml | 18 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 |
2 files changed, 13 insertions, 9 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 87d844edb3..a8088dae36 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -130,19 +130,23 @@ module Make(T : Task) () = struct (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv" - | "-compile" | "-compile-verbose" + | "-require-import" | "-require-export" | "-ri" | "-re" + | "-load-vernac-object" + | "-set" | "-unset" | "-compat" | "-mangle-names" | "-diffs" | "-w" | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j" | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience" | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold" | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl -> set_slave_opt tl + (* Options to discard: 2 arguments *) + | ( "-rifrom" | "-refrom" | "-rfrom" + | "-require-import-from" | "-require-export-from") :: _ :: _ :: tl -> + set_slave_opt tl (* We need to pass some options with one argument *) - | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from" - | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object" - | "-w" | "-color" | "-init-file" - | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" - | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> + | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" + | "-color" | "-init-file" + | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" + | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl (* We need to pass some options with two arguments *) | ( "-R" | "-Q" as x) :: a1 :: a2 :: tl -> diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e69b21a195..732ad05b26 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -50,10 +50,10 @@ let print_usage_common co command = \n -require-export lib, -re lib\ \n load and transitively import Coq library lib\ \n (equivalent to Require Export lib.)\ -\n -require-import-from root lib, -rifrom lib\ +\n -require-import-from root lib, -rifrom root lib\ \n load and import Coq library lib\ \n (equivalent to From root Require Import lib.)\ -\n -require-export-from root lib, -refrom lib\ +\n -require-export-from root lib, -refrom root lib\ \n load and transitively import Coq library lib\ \n (equivalent to From root Require Export lib.)\ \n\ |