From f5dc54519f2a62bab2f7b9059e8c3c8dc53619be Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 00:01:19 +0200
Subject: Fixing printing of surrounding parentheses in "ltac:".

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7e903d2d3d..d1039c1277 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1278,7 +1278,7 @@ module Make
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+            keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))
 
         in pr_tac
 
-- 
cgit v1.2.3