diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index bc3e8ca561..a4ed4f6c58 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -372,6 +372,7 @@ let useInversionLemma = fun id c -> gentac [Identifier id;Constr c] let lemInvIn id c ids gls = + let hyps = List.map (pf_get_hyp gls) ids in let intros_replace_ids gls = let nb_of_new_hyp = nb_prod (pf_concl gls) - List.length ids in if nb_of_new_hyp < 1 then @@ -380,7 +381,7 @@ let lemInvIn id c ids gls = (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls in (* try *) - ((tclTHEN (tclTHEN (bring_hyps ids) (lemInv id c)) + ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) (intros_replace_ids)) gls) (* with Not_found -> errorlabstrm "LemInvIn" (not_found_message ids) | UserError(a,b) -> errorlabstrm "LemInvIn" b |