diff options
| author | Hugo Herbelin | 2016-04-17 22:21:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-19 09:43:40 +0200 |
| commit | 7f85eb4f4cba0194f68034d6ccc0de0be9b5f067 (patch) | |
| tree | f557903ae68a145da6d1c2416f5e520cb9aa5c89 | |
| parent | d926105c022177b70578982d037b12e5d914922b (diff) | |
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.
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |