diff options
| author | Pierre-Marie Pédrot | 2021-01-07 00:18:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-12 13:20:29 +0100 |
| commit | b721752d10969dc70eb21ddad9d794042ea34c59 (patch) | |
| tree | 4cb82b137264022463461e01407b31ddf28551a2 | |
| parent | 71b5649acf83acb3fe6f1c5ddc468d5c504b7983 (diff) | |
Slight tweak of the matching algorithm for PIf vs. Case.
It is equivalent but makes the code more similar to the PCase vs. Case case (aha).
| -rw-r--r-- | pretyping/constr_matching.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c649e25d54..e084c730a9 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 |