3 files changed, 13 insertions, 2 deletions
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