From 3f64bf1be849d1c4040b4d06a3417abd1a57f7d2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 7 Jul 2016 17:54:03 +0200
Subject: Do not display goals in -compile-verbose mode (bug #4841).

The -verbose family of options is only meant to echo sentences as they are
processed. The patch below broke this, while fixing another issue. That
other issue will be fixed in the next commit.

Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its"

This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
---
 toplevel/vernac.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7c4920dfb8..f80aedbf3c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -199,7 +199,7 @@ let display_cmd_header loc com =
 	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com verbose checknav (loc,com) =
+let rec vernac_com checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -223,7 +223,7 @@ let rec vernac_com verbose checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp verbose (loc,v)
+    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
@@ -250,7 +250,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com verbosely checknav loc_ast;
+      vernac_com checknav loc_ast;
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
@@ -275,7 +275,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+let eval_expr loc_ast = vernac_com checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
-- 
cgit v1.2.3