diff options
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 38 |
1 files changed, 30 insertions, 8 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c77feeafbb..15d1ddb4ec 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -352,10 +352,9 @@ let matches_core env sigma allow_bound_rels (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) -> - let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in - let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in - let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in - let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in + let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in + let ctx_b2,b2 = br2.(0) in + let ctx_b2',b2' = br2.(1) in let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then @@ -370,7 +369,7 @@ let matches_core env sigma allow_bound_rels raise PatternMatchingFailure | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) -> - let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in + let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in let n2 = Array.length br2 in let () = match ci1.cip_ind with | None -> () @@ -383,14 +382,37 @@ let matches_core env sigma allow_bound_rels if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) then raise PatternMatchingFailure in + let sorec_under_ctx subst (n, c1) (decls, c2) = + let env = push_rel_context decls env in + let rec fold (ctx, subst) nas decls = match nas, decls with + | [], _ -> + (* Historical corner case: less bound variables are allowed in + destructuring let-bindings. See #13735. *) + (ctx, subst) + | na1 :: nas, d :: decls -> + let na2 = Context.Rel.Declaration.get_annot d in + let t = Context.Rel.Declaration.get_type d in + let ctx = push_binder na1 na2 t ctx in + let subst = add_binders na1 na2 binding_vars subst in + fold (ctx, subst) nas decls + | _, [] -> + assert false + in + let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in + sorec ctx env subst c1 c2 + in let chk_branch subst (j,n,c) = (* (ind,j+1) is normally known to be a correct constructor and br2 a correct match over the same inductive *) assert (j < n2); - sorec ctx env subst c br2.(j) + sorec_under_ctx subst (n, c) br2.(j) + in + let subst = sorec ctx env subst a1 a2 in + let subst = match p1 with + | None -> subst + | Some p1 -> sorec_under_ctx subst p1 p2 in - let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in - List.fold_left chk_branch chk_head br1 + List.fold_left chk_branch subst br1 | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) when Array.equal Int.equal ln1 ln2 && i1 = i2 -> |