summaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /printing/pptactic.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'printing/pptactic.ml')
-rw-r--r--printing/pptactic.ml9
1 files changed, 4 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8264e5a..a669aef9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1260,13 +1260,12 @@ module Make
and pr_tacarg = function
| TacDynamic (loc,t) ->
- pr_with_comments loc (
- str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
- )
+ pr_with_comments loc
+ (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
| MetaIdArg (loc,true,s) ->
- pr_with_comments loc (str ("$" ^ s))
+ pr_with_comments loc (str "$" ++ str s)
| MetaIdArg (loc,false,s) ->
- pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s))
+ pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
| Reference r ->
pr.pr_reference r
| ConstrMayEval c ->