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
---
 test-suite/output/Notations4.out | 2 ++
 test-suite/output/Notations4.v   | 7 +++++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index c1b9a2b1c6..ba4ac5a8f9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -57,3 +57,5 @@ where
      |- Type] (pat, p0, p cannot be used)
 ?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
       |- Type] (pat, p0, p cannot be used)
+fun '{| |} => true
+     : R -> bool
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d1063bfd04..4b9d0abd95 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y.
 Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
 
 End K.
+
+Module EmptyRecordSyntax.
+
+Record R := { n : nat }.
+Check fun '{|n:=x|} => true.
+
+End EmptyRecordSyntax.
-- 
cgit v1.2.3