From afab44873b7861d542cc0146d2bb8099d513f008 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:34:39 +0100
Subject: Fixing printing of "ltac:" in tactics after surrounding parentheses
 became mandatory.

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index fedc62f44f..fcc30d702f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1217,7 +1217,7 @@ module Make
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")"
+            hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
 
         in pr_tac
 
-- 
cgit v1.2.3