From b721752d10969dc70eb21ddad9d794042ea34c59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Jan 2021 00:18:16 +0100
Subject: 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).
---
 pretyping/constr_matching.ml | 7 +++----
 1 file 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
-- 
cgit v1.2.3