From a277da239514ad3bcabc7933a14cfcdc46f272e5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 10:54:20 +0100
Subject: Properly parenthesize "ltac:" arguments (bug #5169).

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1e618b59eb..6e40e03f5b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1216,7 +1216,7 @@ module Make
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+            str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")"
 
         in pr_tac
 
-- 
cgit v1.2.3