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
---
 parsing/g_constr.mlg | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 470782a7dc..d377bd8561 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -393,7 +393,6 @@ GRAMMAR EXTEND Gram
   ;
   record_patterns:
     [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
-      | p = record_pattern; ";" -> { [p] }
       | p = record_pattern-> { [p] }
       | -> { [] }
     ] ]
-- 
cgit v1.2.3