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

2 files changed, 9 insertions, 0 deletions

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.