aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-12-08 18:12:27 +0100
committerPierre-Marie Pédrot2015-12-08 18:12:27 +0100
commite70165079e8defe490a568ece20a7029e4c1626e (patch)
tree7e8ad97cbe6e06251fae9cc2da48acc8ab36d303 /printing
parent071a458681254716a83b1802d5b6a30edda37892 (diff)
parent19ea51a4b7f7debbe5bdeb2b2689cddadd9876f4 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ea705e335e..663b8b8101 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -638,13 +638,13 @@ end) = struct
| CLetTuple (_,nal,(na,po),c,b) ->
return (
hv 0 (
- keyword "let" ++ spc () ++
- hov 0 (str "(" ++
+ hov 2 (keyword "let" ++ spc () ++
+ hov 1 (str "(" ++
prlist_with_sep sep_v pr_lname nal ++
str ")" ++
- pr_simple_return_type (pr mt) na po ++ str " :=" ++
- pr spc ltop c ++ spc ()
- ++ keyword "in") ++
+ pr_simple_return_type (pr mt) na po ++ str " :=") ++
+ pr spc ltop c
+ ++ keyword " in") ++
pr spc ltop b),
lletin
)