3 files changed, 6 insertions, 6 deletions
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