From 220c14e972a4f46003a4d85496b2f107354b4471 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 26 Oct 2010 08:57:05 +0000
Subject: Fail, when successful, prints something only in verbose mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13583 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 57fa29e162..1df58a10ae 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -170,7 +170,7 @@ let rec vernac_com interpfun (loc,com) =
 	  | e ->
 	      (* if [e] is an anomaly, the next function will re-raise it *)
 	      let msg = Cerrors.explain_exn_no_anomaly e in
-	      msgnl (str "The command has indeed failed with message:" ++
+	      if_verbose msgnl (str "The command has indeed failed with message:" ++
 		     fnl () ++ str "=> " ++ hov 0 msg)
 	end
 
-- 
cgit v1.2.3