Fix behaviour of destruct after change of case representation.

We ensure not to generate dummy beta-cuts in case branches generated
by destruct. There was seemingly code trying to perform this but in
an akward way.

1 files changed, 3 insertions, 11 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index cb67d42bdc..8b31c07f5e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -478,13 +478,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
   | App (f,cl) -> (f, cl)
   | _ -> (c,[||]) in
   Array.fold_left3
-    (fun (lacc,sigma,bacc) ty fi l ->
-        if isMeta (strip_outer_cast fi) then
-          (* Support for non-eta-let-expanded Meta as found in *)
-          (* destruct/case with an non eta-let expanded elimination scheme *)
-          let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in
-          r,s,(fi'::bacc)
-        else
+    (fun (lacc,sigma,bacc) ty fi n ->
         (* Deal with a branch in expanded form of the form
            Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
            if it were not so, so as to preserve compatibility with when
@@ -493,7 +487,6 @@ and treat_case ~check env sigma ci lbrty lf acc' =
            CAUTION: it does not deal with the general case of eta-zeta
            reduced branches having a form different from Meta, as it
            would be theoretically the case with third-party code *)
-        let n = List.length l in
         let ctx, body = Term.decompose_lam_n_decls n fi in
         let head, args = decompose_app_vect body in
         (* Strip cast because clenv_cast_meta adds a cast when the branch is
@@ -502,8 +495,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
         let head = strip_outer_cast head in
         if isMeta head then begin
           assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
-          let head' = lift (-n) head in
-          let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in
+          let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head in
           let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
           (r,s,fi'::bacc)
         end
@@ -512,7 +504,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
           let sigma, t'ty = goal_type_of ~check env sigma fi in
           let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in
           (lacc,sigma,fi::bacc))
-    (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
+    (acc',sigma,[]) lbrty lf ci.ci_cstr_ndecls
 
 let convert_hyp ~check ~reorder env sigma d =
   let id = NamedDecl.get_id d in