From 7bc3fb4def33b846b7ac01efe7e42ae6617d46d7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:47:15 +0200
Subject: Fix record pattern interpretation with implicit arguments

We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where
the `_` stands for the parameters).

Fix #12534
---
 test-suite/bugs/closed/bug_12534.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12534.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_12534.v b/test-suite/bugs/closed/bug_12534.v
new file mode 100644
index 0000000000..a55515feb6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12534.v
@@ -0,0 +1,9 @@
+Record C {PROP: Prop} (P : PROP) : Type := { c : unit}.
+Check fun '{|c:=x|} => tt.      (* Fine *)
+Arguments Build_C {_ _} _.
+Check fun '(Build_C _) => tt. (* Works. Note: just 1 argument! *)
+Check fun '{|c:=x|} => tt.
+(* Error: The constructor @Build_C (in type @C) expects 1 argument. *)
+
+Set Asymmetric Patterns.
+Check fun '{|c:=x|} => tt.
-- 
cgit v1.2.3