Use make_case_or_project in auto_ind_decl

Towards #5154 (but insufficient)

4 files changed, 61 insertions, 29 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 0d038e9a67..162d189136 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -365,6 +365,8 @@ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Cons
 
 val of_case_invert : Constr.case_invert -> case_invert
 
+val of_constr_array : Constr.t array -> t array
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d02b015604..2e678f5700 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -347,37 +347,50 @@ let make_case_invert env (IndType (((ind,u),params),indices)) ci =
   then CaseInvert {indices=Array.of_list indices}
   else NoInvert
 
+let make_project env sigma ind pred c branches ps =
+  let open EConstr in
+  assert(Array.length branches == 1);
+  let na, ty, t = destLambda sigma pred in
+  let () =
+    let mib, _ = Inductive.lookup_mind_specif env ind in
+    if (* dependent *) not (Vars.noccurn sigma 1 t) &&
+         not (has_dependent_elim mib) then
+      user_err ~hdr:"make_case_or_project"
+        Pp.(str"Dependent case analysis not allowed" ++
+              str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
+  in
+  let branch = branches.(0) in
+  let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
+  let n, len, ctx =
+    List.fold_right
+      (fun decl (i, j, ctx) ->
+        match decl with
+        | LocalAssum (na, ty) ->
+           let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+           (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+        | LocalDef (na, b, ty) ->
+           (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+      ctx (0, 1, [])
+  in
+  mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
+
+let simple_make_case_or_project env sigma ci pred invert c branches =
+  let open EConstr in
+  let ind = ci.ci_ind in
+  let projs = get_projections env ind in
+  match projs with
+  | None -> mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
+  | Some ps -> make_project env sigma ind pred c branches ps
+
 let make_case_or_project env sigma indt ci pred c branches =
   let open EConstr in
   let IndType (((ind,_),_),_) = indt in
   let projs = get_projections env ind in
   match projs with
-  | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
-  | Some ps ->
-     assert(Array.length branches == 1);
-     let na, ty, t = destLambda sigma pred in
-     let () =
-       let mib, _ = Inductive.lookup_mind_specif env ind in
-       if (* dependent *) not (Vars.noccurn sigma 1 t) &&
-          not (has_dependent_elim mib) then
-       user_err ~hdr:"make_case_or_project"
-                    Pp.(str"Dependent case analysis not allowed" ++
-                     str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
-     in
-     let branch = branches.(0) in
-     let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
-     let n, len, ctx =
-       List.fold_right
-         (fun decl (i, j, ctx) ->
-          match decl with
-          | LocalAssum (na, ty) ->
-             let t = mkProj (Projection.make ps.(i) true, mkRel j) in
-             (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
-          | LocalDef (na, b, ty) ->
-             (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
-         ctx (0, 1, [])
-     in
-     mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
+  | None ->
+     let invert = make_case_invert env indt ci in
+     mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
+  | Some ps -> make_project env sigma ind pred c branches ps
 
 (* substitution in a signature *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8e83814fa0..59ef8e08e3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -212,6 +212,12 @@ val make_case_or_project :
   env -> evar_map -> inductive_type -> case_info ->
   (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
+(** Sometimes [make_case_or_project] is nicer to call with a pre-built
+   [case_invert] than [inductive_type]. *)
+val simple_make_case_or_project :
+  env -> evar_map -> case_info ->
+  (* pred *) EConstr.constr -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
+
 val make_case_invert : env -> inductive_type -> case_info
   -> EConstr.case_invert
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9a50a962b6..f600432c80 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -349,14 +349,25 @@ let build_beq_scheme mode kn =
             (ff ())
             (constrsj.(j).cs_args))
       in
+      let pred = EConstr.of_constr (do_predicate rel_list nb_cstr_args) in
+      let case =
+        simple_make_case_or_project env (Evd.from_env env)
+          ci pred NoInvert (EConstr.mkVar (Id.of_string "Y"))
+          (EConstr.of_constr_array ar2)
+      in
       List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-        (mkCase (Inductive.contract_case env (ci,do_predicate rel_list nb_cstr_args,
-                                              NoInvert, mkVar (Id.of_string "Y") ,ar2)))
+        (EConstr.Unsafe.to_constr case)
         (constrsi.(i).cs_args))
     in
+    let pred = EConstr.of_constr (do_predicate rel_list 0) in
+    let case =
+      simple_make_case_or_project env (Evd.from_env env)
+        ci pred NoInvert (EConstr.mkVar (Id.of_string "X"))
+        (EConstr.of_constr_array ar)
+    in
     mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
         mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
+            (EConstr.Unsafe.to_constr case)))
   in (* build_beq_scheme *)
 
   let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and