From 7f85eb4f4cba0194f68034d6ccc0de0be9b5f067 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Apr 2016 22:21:54 +0200
Subject: Revert "Fixing printing of surrounding parentheses in "ltac:"."

I made a confusion between ltac: in constr and ltac: in tactics, the
one needing parentheses in v8.5 but the latter needing parentheses
only in trunk.

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index d1039c1277..7e903d2d3d 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:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))
+            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
 
         in pr_tac
 
-- 
cgit v1.2.3