From e91327a01f725f6c709adba9ddf3b41212b488ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 16 Sep 2015 08:42:14 +0200
Subject: 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.
---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3