From 6f6b67d3f772205d9481436d62efb6074e975555 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 19 Oct 2015 11:17:56 +0200
Subject: Function debug mode more formatted.

---
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 plugins/funind/invfun.ml                       | 4 ++--
 plugins/funind/recdef.ml                       | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 169a706005..c9dd18a2fc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -52,10 +52,10 @@ let rec print_debug_queue e =
       let _ =
 	match e with
 	| Some e ->
-	   Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	   Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
 	| None ->
 	   begin
-	     Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	     Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
 	   end in
       print_debug_queue None ;
     end
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d979401424..d074bbabd8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -70,8 +70,8 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = Errors.push reraise in
     let e = Cerrors.process_vernac_interp_error reraise in
-    observe (str "observation "++ s++str " raised exception " ++
-	     Errors.iprint e ++ str " on goal " ++ goal );
+    observe (hov 0 (str "observation "++ s++str " raised exception " ++
+	     Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ac7140b9b4..aaeb577d39 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -212,10 +212,10 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
       else
 	begin
-	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	  Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
 	end;
       (* print_debug_queue false e; *)
     end
-- 
cgit v1.2.3