Enforce the argument of elim functions to be a variable.

3 files changed, 10 insertions, 16 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 852ad626e1..f812cb544e 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -34,14 +34,14 @@ 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) =
+    rec_flag allnames tac predicate ind (id, 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
+  let indclause = mk_clenv_from gl (mkVar id, 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 =
@@ -116,16 +116,16 @@ let elim_on_ba tac ba =
   tac branches
   end
 
-let elimination_then tac c =
+let elimination_then tac id =
   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 (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl (mkVar id)) 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)
+  general_elim_then_using mkelim isrec None tac None ind (id, t)
   end
 
 (* Supposed to be called without as clause *)
@@ -168,14 +168,11 @@ Another example :
    Qed.
 *)
 
-let elimHypThen tac id =
-  elimination_then tac (mkVar id)
-
 let rec general_decompose_on_hyp recognizer =
   ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
 
 and general_decompose_aux recognizer id =
-  elimHypThen
+  elimination_then
     (introElimAssumsThen
        (fun bas ->
           tclTHEN (clear [id])
@@ -236,9 +233,6 @@ let h_decompose_and = decompose_and
 
 (* The tactic Double performs a double induction *)
 
-let simple_elimination c =
-  elimination_then (fun _ -> tclIDTAC) c
-
 let induction_trailer abs_i abs_j bargs =
   tclTHEN
     (tclDO (abs_j - abs_i) intro)
@@ -261,7 +255,7 @@ let induction_trailer abs_i abs_j bargs =
           in
           let ids = List.rev (ids_of_named_context hyps) in
           (tclTHENLIST
-            [revert ids; simple_elimination (mkVar id)])
+            [revert ids; elimination_then (fun _ -> tclIDTAC) id])
           end
           ))
 
@@ -279,7 +273,7 @@ let double_ind h1 h2 =
      (onLastHypId
         (fun id ->
            elimination_then
-             (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
+             (introElimAssumsThen (induction_trailer abs_i abs_j)) id)))
   end
 
 let h_double_induction = double_ind
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 4c5cdc8a31..737bbdf728 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -16,7 +16,7 @@ open Tactypes
 
 val case_tac : bool -> or_and_intro_pattern option ->
   (intro_patterns -> named_context -> unit Proofview.tactic) ->
-  constr -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
+  constr -> inductive * EInstance.t -> Id.t * types -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f77b52b931..1bb8158e07 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -490,7 +490,7 @@ let raw_inversion inv_kind id status names =
     tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (tclTHENS
         (assert_before Anonymous cut_concl)
-        [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (c,t);
+        [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (id, t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
   end