1 files changed, 8 insertions, 0 deletions
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;