Put the "move" tactic in the monad.

3 files changed, 10 insertions, 11 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index b7fc63cd5..ce28eacc0 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -200,10 +200,10 @@ END
 (** Move *)
 
 TACTIC EXTEND move
-  [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ]
+  [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
+| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
+| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
+| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
 (** Revert *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 83b8aacfe..15f465ae2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -313,7 +313,7 @@ let apply_clear_request clear_flag dft c =
   else Tacticals.New.tclIDTAC
 
 (* Moving hypotheses *)
-let move_hyp id dest gl = Tacmach.move_hyp id dest gl
+let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
@@ -908,9 +908,8 @@ let find_intro_names ctxt gl =
 let build_intro_tac id dest tac = match dest with
   | MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id)
   | dest -> Tacticals.New.tclTHENLIST 
-    [introduction id; 
-     Proofview.V82.tactic (move_hyp id dest); tac id]
-    
+    [introduction id; move_hyp id dest; tac id]
+
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -1011,7 +1010,7 @@ let intro_replacing id =
   Tacticals.New.tclTHENLIST [
     clear_for_replacing [id];
     introduction id;
-    Proofview.V82.tactic (move_hyp id next_hyp);
+    move_hyp id next_hyp;
   ]
   end }
 
@@ -2437,7 +2436,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
 and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
-      (fun id -> Proofview.V82.tactic (move_hyp id destopt))
+      (fun id -> move_hyp id destopt)
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 046a15d14..24aca2a68 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -170,7 +170,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> unit Proofview.tactic
 
-val move_hyp      : Id.t -> Id.t move_location -> tactic
+val move_hyp      : Id.t -> Id.t move_location -> unit Proofview.tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic