diff options
| author | Enrico Tassi | 2021-01-06 14:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | b9bac1d7ef4a4c06ebe842ffd9aac322186a65d3 (patch) | |
| tree | f29e86bd00ca4ad1ec0d4d1e45b1b523957a665a /sysinit | |
| parent | 4c4d6cfacf92b555546055a45edc19b68245b83c (diff) | |
[coqc] move -output-context from sysinit/coqargs to coqc proper
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 5 | ||||
| -rw-r--r-- | sysinit/coqargs.mli | 1 |
2 files changed, 1 insertions, 5 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 32025ac434..bb0c4882e6 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -93,7 +93,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { @@ -143,7 +142,6 @@ let default_queries = [] let default_post = { memory_stat = false; - output_context = false; } let default = { @@ -440,10 +438,9 @@ let parse_args ~usage ~init arglist : t * string list = warn_deprecated_sprop_cumul(); add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval - |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} + |"-m"|"--memory" -> { oval with post = { memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} |"-boot" -> { oval with pre = { oval.pre with boot = true }} - |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} |"-quiet"|"-silent" -> diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index ebf367270d..acf941f730 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -74,7 +74,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { |