diff options
| -rw-r--r-- | interp/constrextern.ml | 23 | ||||
| -rw-r--r-- | test-suite/output/Record.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Record.v | 5 |
3 files changed, 24 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85e..0ba056a878 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 diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 36d643a447..37b4fb25f7 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -14,3 +14,9 @@ build 5 : test_r build_c 5 : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 6aa3df9830..c3d9f1e573 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -19,3 +19,8 @@ Check build 5. Check {| field := 5 |}. Check build_r 5. Check build_c 5. + +Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). |