1 files changed, 125 insertions, 13 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 415c980c2a..852ad626e1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -10,33 +10,145 @@
 
 open Util
 open Names
+open Constr
 open Termops
 open EConstr
 open Inductiveops
 open Hipattern
 open Tacmach.New
 open Tacticals.New
+open Clenv
 open Tactics
 open Proofview.Notations
 
+type branch_args = {
+  ity        : pinductive;   (* the type we were eliminating on *)
+  branchnum  : int;         (* the branch number *)
+  nassums    : int;         (* number of assumptions/letin to be introduced *)
+  branchsign : bool list;   (* the signature of the branch.
+                               true=assumption, false=let-in *)
+  branchnames : Tactypes.intro_patterns}
+
 module NamedDecl = Context.Named.Declaration
 
+(* Find the right elimination suffix corresponding to the sort of the goal *)
+(* c should be of type A1->.. An->B with B an inductive definition *)
+let general_elim_then_using mk_elim
+    rec_flag allnames tac predicate ind (c, t) =
+  let open Pp in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma, elim = mk_elim ind gl in
+  let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (Proofview.Goal.enter begin fun gl ->
+  let indclause = mk_clenv_from gl (c, t) in
+  (* applying elimination_scheme just a little modified *)
+  let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim)  in
+  let indmv =
+    match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
+    | Meta mv -> mv
+    | _         -> CErrors.anomaly (str"elimination.")
+  in
+  let pmv =
+    let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
+    match EConstr.kind elimclause.evd p with
+    | Meta p -> p
+    | _ ->
+        let name_elim =
+          match EConstr.kind sigma elim with
+          | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
+          | _ -> mt ()
+        in
+        CErrors.user_err ~hdr:"Tacticals.general_elim_then_using"
+          (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
+  in
+  let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
+  let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in
+  let brnames = Tacticals.compute_induction_names false branchsigns allnames in
+  let flags = Unification.elim_flags () in
+  let elimclause' =
+    match predicate with
+    | None   -> elimclause'
+    | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
+  in
+  let after_tac i =
+    let ba = { branchsign = branchsigns.(i);
+                branchnames = brnames.(i);
+                nassums = List.length branchsigns.(i);
+                branchnum = i+1;
+                ity = ind; }
+    in
+    tac ba
+  in
+  let branchtacs = List.init (Array.length branchsigns) after_tac in
+  Proofview.tclTHEN
+    (Clenv.res_pf ~flags elimclause')
+    (Proofview.tclEXTEND [] tclIDTAC branchtacs)
+  end) end
+
+(* computing the case/elim combinators *)
+
+let gl_make_elim ind = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in
+  let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+  (sigma, c)
+end
+
+let gl_make_case dep (ind, u) = begin fun gl ->
+  let sigma = project gl in
+  let u = EInstance.kind (project gl) u in
+  let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) dep
+    (elimination_sort_of_goal gl)
+  in
+  (sigma, EConstr.of_constr r)
+end
+
+let make_elim_branch_assumptions ba hyps =
+  let assums =
+    try List.rev (List.firstn ba.nassums hyps)
+    with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in
+  assums
+
+let elim_on_ba tac ba =
+  Proofview.Goal.enter begin fun gl ->
+  let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+  tac branches
+  end
+
+let elimination_then tac c =
+  let open Declarations in
+  Proofview.Goal.enter begin fun gl ->
+  let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
+  let isrec,mkelim =
+    match (Global.lookup_mind (fst (fst ind))).mind_record with
+    | NotRecord -> true,gl_make_elim
+    | FakeRecord | PrimRecord _ -> false,gl_make_case true
+  in
+  general_elim_then_using mkelim isrec None tac None ind (c, t)
+  end
+
 (* Supposed to be called without as clause *)
 let introElimAssumsThen tac ba =
-  assert (ba.Tacticals.branchnames == []);
-  let introElimAssums = tclDO ba.Tacticals.nassums intro in
+  assert (ba.branchnames == []);
+  let introElimAssums = tclDO ba.nassums intro in
   (tclTHEN introElimAssums (elim_on_ba tac ba))
 
 (* Supposed to be called with a non-recursive scheme *)
 let introCaseAssumsThen with_evars tac ba =
-  let n1 = List.length ba.Tacticals.branchsign in
-  let n2 = List.length ba.Tacticals.branchnames in
+  let n1 = List.length ba.branchsign in
+  let n2 = List.length ba.branchnames in
   let (l1,l2),l3 =
-    if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
-    else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
+    if n1 < n2 then List.chop n1 ba.branchnames, []
+    else (ba.branchnames, []), List.make (n1-n2) false in
   let introCaseAssums =
     tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
-  (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
+  (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba))
+
+let case_tac dep names tac elim ind c =
+  let mkcase = gl_make_case dep in
+  let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in
+  general_elim_then_using mkcase false names tac (Some elim) ind c
 
 (* The following tactic Decompose repeatedly applies the
    elimination(s) rule(s) of the types satisfying the predicate
@@ -68,7 +180,7 @@ and general_decompose_aux recognizer id =
        (fun bas ->
           tclTHEN (clear [id])
             (tclMAP (general_decompose_on_hyp recognizer)
-               (ids_of_named_context bas.Tacticals.assums))))
+               (ids_of_named_context bas))))
     id
 
 (* We should add a COMPLETE to be sure that the created hypothesis
@@ -82,10 +194,10 @@ let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
   let typc = pf_get_type_of gl c in
   tclTHENS (cut typc)
-    [ tclTHEN (intro_using tmphyp_name)
-         (onLastHypId
-            (ifOnHyp recognizer (general_decompose_aux recognizer)
-              (fun id -> clear [id])));
+    [ intro_using_then tmphyp_name (fun id ->
+          ifOnHyp recognizer (general_decompose_aux recognizer)
+            (fun id -> clear [id])
+            id);
        exact_no_check c ]
   end
 
@@ -136,7 +248,7 @@ let induction_trailer abs_i abs_j bargs =
           let idty = pf_get_type_of gl (mkVar id) in
           let fvty = global_vars (pf_env gl) (project gl) idty in
           let possible_bring_hyps =
-            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
+            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
           in
           let (hyps,_) =
             List.fold_left