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
---
 interp/constrintern.ml             | 6 +++---
 test-suite/bugs/closed/bug_12534.v | 9 +++++++++
 2 files changed, 12 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_12534.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ee041ed088..1e64d78f94 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv =
         | None -> DAst.make ?loc @@ RCPatAtom None
         | Some (n, head, pl) ->
           let pl =
-            if get_asymmetric_patterns () then pl else
             let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
-            List.rev_append pars pl in
+            List.rev_append pars pl
+          in
           let (_,argscs) = find_remaining_scopes [] pl head in
           let pats = List.map2 (in_pat_sc scopes) argscs pl in
-          DAst.make ?loc @@ RCPatCstr(head, [], pats)
+          DAst.make ?loc @@ RCPatCstr(head, pats, [])
       end
     | CPatCstr (head, None, pl) ->
       begin
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