From cf7b845b433ea0aeb97430093c51ec77c3d1c4af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 16:28:10 +0000
Subject: Check bavard meme en mode silencieux, car on l'a voulu

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5b84e9311f..94bdb1a083 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -828,12 +828,12 @@ let vernac_check_may_eval redexp glopt rc =
   match redexp with
     | None ->
 	if !pcoq <> None then (out_some !pcoq).print_check j
-	else Options.if_verbose msg (print_judgment env j)
+	else msg (print_judgment env j)
     | Some r ->
 	let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in
 	if !pcoq <> None
 	then (out_some !pcoq).print_eval (redfun env evmap) env rc j
-	else Options.if_verbose msg (print_eval redfun env j)
+	else msg (print_eval redfun env j)
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
-- 
cgit v1.2.3