From 48d0870c093a15faaf3dbb327afa94f5da2a38ea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2011 15:38:38 +0000
Subject: Improving pretty-printing of Ltac functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14801 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f55ced8090..3305acb779 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -906,8 +906,8 @@ let rec pr_tac inherited tac =
              pr_tac (lorelse,E) t2),
       lorelse
   | TacFail (n,l) ->
-      str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
-      prlist (pr_arg (pr_message_token pr_ident)) l, latom
+      hov 1 (str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+      prlist (pr_arg (pr_message_token pr_ident)) l), latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
   | TacSolve tl ->
-- 
cgit v1.2.3