diff options
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)) |