aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index 6230fa0606..85740f187b 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -1083,7 +1083,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