diff options
| author | Guillaume Melquiond | 2015-09-16 06:41:04 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-09-16 06:41:04 +0200 |
| commit | 6af9f644b64acf485c1628247f5435d09b990b79 (patch) | |
| tree | b86eedd867c0811f9b29d6a8e4dbc79ee87d9063 /interp | |
| parent | 42ab65d7c7eed4f6696dacedceaf7c695e0d06d6 (diff) | |
Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #4268)
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ecaf2b8c13..c754f1910c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in begin match sorted_fields with | None -> RCPatAtom (loc, None) - | Some (_, head, pl) -> + | Some (n, head, pl) -> + let pl = + if !oldfashion_patterns then pl else + let pars = List.make n (CPatAtom (loc, None)) in + List.rev_append pars pl in match drop_syndef top env head pl with |Some (a,b,c) -> RCPatCstr(loc, a, b, c) |None -> raise (InternalizationError (loc,NotAConstructor head)) |