From cddddce068bc0482f62ffab8e412732a307b90bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 May 2016 10:47:53 +0200
Subject: Put the "move" tactic in the monad.

---
 ltac/coretactics.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'ltac')

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index b7fc63cd56..ce28eacc09 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 *)
-- 
cgit v1.2.3