From 0cd0c393b12478cbf794f84bed5945f6fa7a8f39 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 7 Oct 2013 16:17:52 +0000
Subject: STM: fix verbosity of queries

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16861 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8abac272c0..1cff1aeb83 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1837,7 +1837,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed!")
 	  | HasFailed msg ->
-	      if_verbose msgnl
+	      if_verbose msg_info
 		(str "The command has indeed failed with message:" ++
 		 fnl () ++ str "=> " ++ hov 0 (str msg))
           | _ -> assert false
@@ -1869,5 +1869,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             Flags.program_mode := orig_program_mode;
             raise e
   in
-    aux false c
+    if verbosely then Flags.verbosely (aux false) c
+    else aux false c
 
-- 
cgit v1.2.3