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

of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).

1 files changed, 16 insertions, 3 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5e99521a1..3fa037ffd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -413,12 +413,25 @@ 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,hd,c1,lc) ->
+  | 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
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | 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))
       | _ -> assert false
       in
-      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in