aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-24 13:37:51 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-24 13:37:51 +0200
commitf7f5b7dcc641e233a1b18dab7228d1d8c55596b3 (patch)
treeb0bf4f02f30ccb2845b114202ec8691c1bc89ea6 /printing
parentbb8dd8212efb839746e050062b108b33632ba224 (diff)
parent1343b69221ce3eeb3154732e73bbdc0044b224a8 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d9d8af66b..650b8f726 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -676,11 +676,11 @@ end) = struct
return (pr_glob_sort s, latom)
| CCast (_,a,b) ->
return (
- hv 0 (pr mt (lcast,L) a ++ cut () ++
+ hv 0 (pr mt (lcast,L) a ++ spc () ++
match b with
- | CastConv b -> str ":" ++ pr mt (-lcast,E) b
- | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
- | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b
+ | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b
| CastCoerce -> str ":>"),
lcast
)