From e3ec13976d39909ac6f1a82bf1b243ba8a895190 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Oct 2015 12:42:27 +0100 Subject: Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" After all, let's target 8.6. --- pretyping/constr_matching.ml | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) (limited to 'pretyping/constr_matching.ml') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 3fa037ffd..5e99521a1 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -413,25 +413,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in let sub = (env, c1) :: subargs env lc in try_aux sub mk_ctx next - | Case (ci,p,c,brs) -> - (* Warning: this assumes predicate and branches to be - in canonical form using let and fun of the signature *) - let nardecls = List.length ci.ci_pp_info.ind_tags in - let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in - let env_p = Environ.push_rel_context sign_p env in - let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in - let sign_brs = Array.map fst brs in - let f (sign,br) = (Environ.push_rel_context sign env, br) in - let sub_br = Array.map f brs in + | Case (ci,hd,c1,lc) -> let next_mk_ctx = function - | c :: p :: brs -> - let p = it_mkLambda_or_LetIn p sign_p in - let brs = - Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in - mk_ctx (mkCase (ci,p,c,brs)) + | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) | _ -> assert false in - let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in + let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in -- cgit v1.2.3