Add support so that the type of a match in an inductive type with let-in

is reduced as if without let-in, when applied to arguments.

This allows e.g. to have a head-betazeta-reduced goal in the following example.

Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)

6 files changed, 32 insertions, 4 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6b4dd536a1..ca814f497c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in
       vargs @ [dep_cstr] in
-    let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+    let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base args in
   Array.mapi build_one_branch mip.mind_nf_lc
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 356a699c66..7f6a4a6442 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -526,7 +526,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ec34383820..2c70a6c9a0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1628,3 +1628,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7c61d4e143..d4f061c5be 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -278,6 +278,7 @@ val whd_meta : evar_map -> constr -> constr
 val plain_instance : constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cd52ba44da..213d7ddda4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma =
     | Ind ind -> rename_type_of_inductive env ind
     | Construct cstr -> rename_type_of_constructor env cstr
     | Case (_,p,c,lf) ->
-        let Inductiveops.IndType(_,realargs) =
+        let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
@@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let t = whd_beta sigma (applist (p, realargs)) in
+        let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in
+        let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
index e66bf922d7..bb673f38c2 100644
--- a/test-suite/bugs/closed/3210.v
+++ b/test-suite/bugs/closed/3210.v
@@ -7,3 +7,16 @@ Definition foo (x : Foo) : bool :=
   match x with
   I => true
   end.
+
+Definition foo' (x : Foo) : x = x.
+case x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+elim x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+induction x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+destruct x.
+match goal with |- I = I => idtac end. (* check form of the goal *)