5 files changed, 14 insertions, 7 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 = {
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index a896541573..a403640149 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -56,7 +56,7 @@ let coqc_main ((copts,_),stm_opts) injections ~opts =
 
   flush_all();
 
-  if opts.Coqargs.post.Coqargs.output_context then begin
+  if copts.Coqcargs.output_context then begin
     let sigma, env = let e = Global.env () in Evd.from_env e, e in
     Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
   end;
@@ -79,7 +79,8 @@ let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqt
   parse_extra = (fun extras ->
     let color_mode, extras = Coqtop.parse_extra_colors extras in
     let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
-    ((Coqcargs.parse extras, color_mode), stm_opts), []);
+    let coqc_opts = Coqcargs.parse extras in
+    ((coqc_opts, color_mode), stm_opts), []);
   usage = coqc_specific_usage;
   init_extra = coqc_init;
   run = coqc_run;
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 402a4d83c9..f84d73ed17 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -25,6 +25,8 @@ type t =
 
   ; outputstate : string option
   ; glob_out    : Dumpglob.glob_output
+
+  ; output_context : bool
   }
 
 let default =
@@ -42,6 +44,8 @@ let default =
 
   ; outputstate = None
   ; glob_out = Dumpglob.MultFiles
+
+  ; output_context = false
   }
 
 let depr opt =
@@ -162,6 +166,10 @@ let parse arglist : t =
           depr opt;
           let _ = next () in
           oval
+
+        (* Non deprecated options *)
+        | "-output-context" ->
+          { oval with output_context = true }
         (* Verbose == echo mode *)
         | "-verbose" ->
           echo := true;
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index a9fc27b1b4..905250e363 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -39,6 +39,8 @@ type t =
 
   ; outputstate : string option
   ; glob_out    : Dumpglob.glob_output
+
+  ; output_context : bool
   }
 
 val default : t