Fixing a bug in intros_replacing which was causing inversion not

necessarily granting names given in the "as" clause.

1 files changed, 22 insertions, 15 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1242e25e45..e671aa3ca4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -603,6 +603,10 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
 let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
 
+let intro_move idopt hto = match idopt with
+  | None -> intro_gen (NamingAvoid []) hto true false
+  | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
+
 (**** Multiple introduction tactics ****)
 
 let rec intros_using = function
@@ -630,34 +634,37 @@ 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 rec get_next_hyp_position id l = function
   | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
       if Id.equal hyp id then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
+	match right with
+        | (id,_,_)::_ -> (try List.assoc id l with Not_found -> MoveBefore id)
+        | [] -> MoveLast
       else
-	get_next_hyp_position id right
+	get_next_hyp_position id l right
 
 let intro_replacing id gl =
-  let next_hyp = get_next_hyp_position id (pf_hyps gl) in
+  let next_hyp = get_next_hyp_position id [] (pf_hyps gl) in
   tclTHENLIST
     [thin_for_replacing [id]; introduction id; move_hyp true id next_hyp] gl
 
+(* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to
+   reintroduce y, y,' y''. Note that we have to clear y, y' and y''
+   before introducing y because y' or y'' can e.g. depend on old y. *)
+
 let intros_replacing ids =
-  let rec introrec = function
-    | [] -> Proofview.tclUNIT()
-    | id::tl ->
-	Tacticals.New.tclTHEN (Tacticals.New.tclORELSE (Proofview.V82.tactic (intro_replacing id)) (intro_using id))
-           (introrec tl)
-  in
-  introrec ids
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let posl = List.fold_right (fun id posl ->
+      (id,get_next_hyp_position id posl hyps) :: posl) ids [] in
+    Tacticals.New.tclTHEN
+      (Proofview.V82.tactic (thin_for_replacing ids))
+      (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
+  end
 
 (* User-level introduction tactics *)
 
-let intro_move idopt hto = match idopt with
-  | None -> intro_gen (NamingAvoid []) hto true false
-  | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
-
 let pf_lookup_hypothesis_as_renamed env ccl = function
   | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n
   | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id