diff options
| author | Emilio Jesus Gallego Arias | 2020-07-17 17:00:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-17 17:00:00 +0200 |
| commit | e04e12c60fe90735c22542bfd6b0b94f4b4cbc1e (patch) | |
| tree | 20b8bf7cfe652b51a1d0ed96f5482f961dcc8b4d | |
| parent | f54bc666c62ad9a66067cb486816cdfc68c2946d (diff) | |
| parent | 7bc3fb4def33b846b7ac01efe7e42ae6617d46d7 (diff) | |
Merge PR #12631: Fix record pattern interpretation with implicit arguments
Reviewed-by: herbelin
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12534.v | 9 |
2 files changed, 12 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 987aa63392..6d4ab8b4d6 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. |