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

After all, let's target 8.6.

2 files changed, 3 insertions, 42 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
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 5bef2e512..6c4d4ae98 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,29 +317,3 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
-
-(* Check that matching "match" does not look into the invisible
-   canonically generated binders of the return clause and of the branches *)
-
-Goal forall n, match n with 0 => true | S _ => false end = true.
-intros. unfold nat_rect.
-Fail match goal with |- context [nat] => idtac end.
-Abort.
-
-(* Check that branches of automatically generated elimination
-   principle are correctly eta-expanded and hence matchable as seen
-   from the user point of view *)
-
-Goal forall a f n, nat_rect (fun _ => nat) a f n = 0.
-intros. unfold nat_rect.
-match goal with |- context [f _] => idtac end.
-Abort.
-
-(* Check that branches of automatically generated elimination
-   principle are in correct form also in the presence of let-ins *)
-
-Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a.
-Goal forall x, match x with c => 0 end = 1.
-intros.
-match goal with |- context [0] => idtac end.
-Abort.