Merge PR #11094: Miscellaneous micro-improvements of the syntax of records

Reviewed-by: ppedrot

4 files changed, 11 insertions, 2 deletions

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] }
       | -> { [] }
     ] ]
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
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.