From 1343b69221ce3eeb3154732e73bbdc0044b224a8 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Wed, 24 Jun 2015 09:30:31 +0200
Subject: Add a space in cast since cast binds loosely.

Fixes bug 3936
This closes #73
---
 printing/ppconstr.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d9d8af66b9..650b8f7262 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
         )
-- 
cgit v1.2.3