From bbb7ebef29cd917029db0c4fe7dda5e58be925b6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Nov 2003 10:06:48 +0000
Subject: Re-suppression de is_verbose dans Print, pour coqide

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5577db4ff9..541422261c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -835,8 +835,7 @@ let vernac_global_check c =
   let j = Safe_typing.typing senv c in
   msg (print_safe_judgment env j)
 
-let vernac_print p = 
-  if Options.is_verbose () then match p with
+let vernac_print = function
   | PrintTables -> print_tables ()
   | PrintLocalContext -> msg (print_local_context ())
   | PrintFullContext -> msg (print_full_context_typ ())
-- 
cgit v1.2.3