1 files changed, 47 insertions, 0 deletions
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
new file mode 100644
index 00000000..db2bbb0d
--- /dev/null
+++ b/test-suite/success/record_syntax.v
@@ -0,0 +1,47 @@
+Module A.
+
+Record Foo := { foo : unit; bar : unit }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt
+|}.
+
+Definition foo0 (p : Foo) := match p with {| |} => tt end.
+Definition foo1 (p : Foo) := match p with {| foo := f |} => f end.
+Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end.
+Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end.
+Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
+
+End A.
+
+Module B.
+
+Record Foo := { }.
+
+End B.
+
+Module C.
+
+Record Foo := { foo : unit; bar : unit; }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt;
+|}.
+
+End C.
+
+Module D.
+
+Record Foo := { foo : unit }.
+Definition foo_ := {| foo := tt |}.
+
+End D.
+
+Module E.
+
+Record Foo := { foo : unit; }.
+Definition foo_ := {| foo := tt; |}.
+
+End E.