Further remove the type Elim.branch_assumptions.

Only one field was used throughout the code base.

3 files changed, 5 insertions, 13 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2fc2c195e0..ee249a3a11 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -30,10 +30,6 @@ type branch_args = {
                                true=assumption, false=let-in *)
   branchnames : Tactypes.intro_patterns}
 
-type branch_assumptions = {
-  ba        : branch_args;       (* the branch args *)
-  assums    : named_context}   (* the list of assumptions introduced *)
-
 module NamedDecl = Context.Named.Declaration
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -122,7 +118,7 @@ let make_elim_branch_assumptions ba hyps =
   let assums =
     try List.rev (List.firstn ba.nassums hyps)
     with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in
-  { ba = ba; assums = assums }
+  assums
 
 let elim_on_ba tac ba =
   Proofview.Goal.enter begin fun gl ->
@@ -201,7 +197,7 @@ and general_decompose_aux recognizer id =
        (fun bas ->
           tclTHEN (clear [id])
             (tclMAP (general_decompose_on_hyp recognizer)
-               (ids_of_named_context bas.assums))))
+               (ids_of_named_context bas))))
     id
 
 (* We should add a COMPLETE to be sure that the created hypothesis
@@ -269,7 +265,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.assums
+            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
           in
           let (hyps,_) =
             List.fold_left
diff --git a/tactics/elim.mli b/tactics/elim.mli
index f66462a224..921a942e72 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -22,10 +22,6 @@ type branch_args = private {
                                 true=assumption, false=let-in *)
   branchnames : intro_patterns}
 
-type branch_assumptions = private {
-  ba        : branch_args;       (** the branch args *)
-  assums    : named_context}   (** the list of assumptions introduced *)
-
 val case_then_using :
   or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
   constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
@@ -35,7 +31,7 @@ val case_nodep_then_using :
   constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
 val introCaseAssumsThen : Tactics.evars_flag ->
-  (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
+  (intro_patterns -> named_context -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 86407c9656..7a88a4b0be 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -409,7 +409,7 @@ let nLastDecls i tac =
 
 let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.enter begin fun gl ->
-  let (depids,nodepids) = split_dep_and_nodep ba.Elim.assums gl in
+  let (depids,nodepids) = split_dep_and_nodep ba gl in
   let first_eq = ref Logic.MoveLast in
   let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
   match othin with