diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-16 23:23:53 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-07 15:18:03 +0200 |
commit | 495bccc436cfe72af9955b4b9d8564a8831850b9 (patch) | |
tree | 88820173b82b67f0974108e299615f138a6e8d24 /interp/constrextern.ml | |
parent | 33f40197e6b7bef02c8df2dc0a0066f8144b66d6 (diff) |
Fixing #4499 (not using unnamed record field in {| |} notation).
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r-- | interp/constrextern.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85..0ba056a87 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -307,16 +307,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = - match projs with - | [] -> acc - | None :: q -> ip q args acc - | Some c :: q -> - match args with - | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc - (* we don't want to have 'x = _' in our patterns *) - | head :: tail -> ip q tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, CPatAtom(_, None) -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc) + | _ -> raise No_match in + ip q tail acc + | _ -> assert false in CPatRecord(loc, List.rev (ip projs args [])) with |