From a821f74dc91e438c86037d1dc8903a49934e6ee5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Apr 2017 02:01:02 +0200
Subject: [flags] Deprecate is_silent/is_verbose in favor of single flag.

Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.

We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
---
 plugins/funind/recdef.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5460d6fb73..9788ccfee2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1590,8 +1590,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
 	functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
-      if Flags.is_verbose ()
-      then msgnl (h 1 (Ppconstr.pr_id function_name ++
+      Flags.if_verbose
+        msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
 		    h 1 (Ppconstr.pr_id equation_id ++
 			   spc () ++ str"is defined" )
-- 
cgit v1.2.3