Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"

After all, let's target 8.6.

1 files changed, 3 insertions, 16 deletions

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