diff options
| author | Hugo Herbelin | 2015-09-16 08:42:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-16 08:48:05 +0200 |
| commit | e91327a01f725f6c709adba9ddf3b41212b488ca (patch) | |
| tree | fa90324319ccd7beb12c446f22fee8ec6be3dc3f /tactics | |
| parent | 95903cc3bcb9aed92459e644d295be4d9ca25405 (diff) | |
Continuing investigation on how to preserve the locality of the action
of "apply ... in ... as ..." in the context.
Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is
created, the statement of the refined hypothesis virtually depends on
the whole context and has to be left at the top.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0235126cc0..d0724804b4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2283,7 +2283,9 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> - let destopt = get_previous_hyp_position id gl in + let destopt = + if with_evars then MoveLast (* evars would depend on the whole context *) + else get_previous_hyp_position id gl in let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = let last,first = List.sep_last lemmas in |