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).

2 files changed, 42 insertions, 3 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5e99521a12..3fa037ffdd 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
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 6c4d4ae98f..5bef2e512a 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,29 @@ 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.