From a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 1 Jun 2012 20:08:33 +0000
Subject: More cleaning

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/functional_principles_proofs.ml | 12 ++----------
 plugins/funind/recdef.ml                       |  3 +--
 2 files changed, 3 insertions(+), 12 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bd5fd9c09c..b8887c68f9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -23,23 +23,15 @@ open Misctypes
 (*
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
-  else ()
-
-let observennl strm =
-  if do_observe ()
-  then begin Pp.msg strm;Pp.pp_flush () end
+  then Pp.msg_debug strm
   else ()
 
-
-
-
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
  with e ->
    let e = Cerrors.process_vernac_interp_error e in
    let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
-   msgnl (str "observation "++ s++str " raised exception " ++
+   msg_debug (str "observation "++ s++str " raised exception " ++
 	    Errors.print e ++ str " on goal " ++ goal );
    raise e;;
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7cf438e6f5..fe359f08d9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1366,7 +1366,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     end;
   try
     by tclIDTAC; (* raises UserError _ if the proof is complete *)
-    if Flags.is_verbose () then (pp (Printer.pr_open_subgoals()))
   with UserError _ ->
     defined ()
 
@@ -1521,7 +1520,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e ->
 	begin
 	  if do_observe ()
-	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
+	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
 	  true
-- 
cgit v1.2.3