Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.

1 files changed, 12 insertions, 11 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5d2a2b1a66..6e414b8e8f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -806,18 +806,21 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   in
   aux n []
 
-let rec get_next_hyp_position id = function
+let get_next_hyp_position id gl =
+  let rec get_next_hyp_position id = function
   | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
-      if Id.equal hyp id then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
-      else
-	get_next_hyp_position id right
+    if Id.equal hyp id then
+      match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
+    else
+      get_next_hyp_position id right
+  in
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  get_next_hyp_position id hyps
 
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let next_hyp = get_next_hyp_position id hyps in
+  let next_hyp = get_next_hyp_position id gl in
   Tacticals.New.tclTHENLIST [
     Proofview.V82.tactic (thin_for_replacing [id]);
     introduction id;
@@ -836,8 +839,7 @@ let intro_replacing id =
 let intros_possibly_replacing ids =
   let suboptimal = true in
   Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let posl = List.map (fun id -> (id,get_next_hyp_position id hyps)) ids in
+    let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
 	Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id])))
@@ -850,8 +852,7 @@ let intros_possibly_replacing ids =
 (* This version assumes that replacement is actually possible *)
 let intros_replacing ids =
   Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let posl = List.map (fun id -> (id,get_next_hyp_position id hyps)) ids in
+    let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
       (Proofview.V82.tactic (thin_for_replacing ids))
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)