diff options
| author | Pierre-Marie Pédrot | 2020-08-29 18:47:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 19:06:33 +0200 |
| commit | 007f760ddc7ad0960e91307d02bfc7fef42dc46b (patch) | |
| tree | 38ed87e533538128b9101115d4a3063fc0f0f1ca /tactics/elim.ml | |
| parent | afb4e0633f7cb36c10356d7da9b915d2e95aee6e (diff) | |
Further remove the type Elim.branch_assumptions.
Only one field was used throughout the code base.
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 10 |
1 files changed, 3 insertions, 7 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 |