diff options
| author | Gaëtan Gilbert | 2020-07-02 15:47:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-02 15:49:08 +0200 |
| commit | 7bc3fb4def33b846b7ac01efe7e42ae6617d46d7 (patch) | |
| tree | 82155eed74bf2a8cfbb3ae032e956891629c1c85 /test-suite/bugs | |
| parent | a1835c755f07b2199d122632360a5d236cd9984e (diff) | |
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
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_12534.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |