From 1e5bae9d78192e3f0c5d7e25ab7e64fdc605316f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 11 Nov 2019 09:57:40 +0100
Subject: Miscellaneous improvements of the syntax of records.

- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
---
 printing/ppconstr.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5ed96dd5e3..2da163b8ee 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -249,7 +249,8 @@ let tag_var = tag Tag.variable
         let pp (c, p) =
           pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
         in
-        str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
+        (if l = [] then str "{| |}"
+         else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
 
       | CPatAlias (p, na) ->
         pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las
-- 
cgit v1.2.3