Writing intro_replacing in the new monad.

2 files changed, 12 insertions, 6 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1ecd279355..5d2a2b1a66 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -814,10 +814,16 @@ let rec get_next_hyp_position id = function
       else
 	get_next_hyp_position id right
 
-let intro_replacing id gl =
-  let next_hyp = get_next_hyp_position id (pf_hyps gl) in
-  tclTHENLIST
-    [thin_for_replacing [id]; Proofview.V82.of_tactic (introduction id); move_hyp id next_hyp] gl
+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
+  Tacticals.New.tclTHENLIST [
+    Proofview.V82.tactic (thin_for_replacing [id]);
+    introduction id;
+    Proofview.V82.tactic (move_hyp id next_hyp);
+  ]
+  end
 
 (* 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''
@@ -4303,7 +4309,7 @@ let symmetry_in id =
           | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
           | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
         Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
-          [ Proofview.V82.tactic (intro_replacing id);
+          [ intro_replacing id;
             Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
     end
     begin function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7a6464547c..52538d041b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -61,7 +61,7 @@ val intro_move_avoid  : Id.t option -> Id.t list -> Id.t move_location -> unit P
      to belong to [idl] *)
 val intro_avoiding       : Id.t list -> unit Proofview.tactic
 
-val intro_replacing      : Id.t -> tactic
+val intro_replacing      : Id.t -> unit Proofview.tactic
 val intro_using          : Id.t -> unit Proofview.tactic
 val intro_mustbe_force   : Id.t -> unit Proofview.tactic
 val intro_then           : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic