3 files changed, 2 insertions, 8 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4fd2b0e92..5ae1c36ed 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -548,7 +548,7 @@ let parse_args arglist =
     |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
-    |"-just-parsing" -> Vernac.just_parsing := true
+    |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
     |"-m"|"--memory" -> memory_stat := true
     |"-noinit"|"-nois" -> load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8230f92a6..b453dbc46 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -122,7 +122,6 @@ let parse_sentence = Flags.with_option Flags.we_are_parsing
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let just_parsing = ref false
 let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
@@ -193,8 +192,6 @@ let rec interp_vernac po chan_beautify checknav (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely f
 
-    | v when !just_parsing -> ()
-
     | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index c9714f8c9..0d9f5871a 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -14,13 +14,10 @@
 val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
  Loc.t * Vernacexpr.vernac_expr
 
-(** Reads and executes vernac commands from a stream.
-   The boolean [just_parsing] disables interpretation of commands. *)
+(** Reads and executes vernac commands from a stream. *)
 
 exception End_of_input
 
-val just_parsing : bool ref
-
 val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)