diff options
| -rw-r--r-- | tactics/elim.ml | 10 | ||||
| -rw-r--r-- | tactics/elim.mli | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 |
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 |