diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 02:41:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-22 14:39:31 +0100 |
| commit | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (patch) | |
| tree | a9e2766e23ccb0afac63edac44f4442a92686501 /checker/checker.ml | |
| parent | fa3a97426013cf940cd25abde43c0191766218b1 (diff) | |
[library] Remove `-boot` option.
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 4dac02210b..3c93ef7d36 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -192,7 +192,6 @@ let print_usage_channel co command = \n -coqlib dir set coqchk's standard library location\ \n -where print coqchk's standard library location and exit\ \n -v print coqchk version and exit\ -\n -boot boot mode\ \n -o, --output-context print the list of assumptions\ \n -m, --memory print the maximum heap size\ \n -silent disable trace of constants being checked\ @@ -320,8 +319,6 @@ let explain_exn = function let deprecated flag = Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) -let boot_opt = ref false - let parse_args argv = let rec parse = function | [] -> () @@ -358,7 +355,6 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot_opt := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem |