Moving the "move" tactic to TACTIC EXTEND.

7 files changed, 9 insertions, 17 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index dae960e0e5..7366bc03e6 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -160,7 +160,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
   (* Conversion *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e50eca25be..0c90a8bca4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -617,8 +617,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Context management *)
-      | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
-	  TacAtom (!@loc, TacMove (hfrom,hto))
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
 
       (* Equality and inversion *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 2c57cb811e..36863906ea 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -892,12 +892,6 @@ module Make
             )
 
           (* Context management *)
-          | TacMove (id1,id2) ->
-            hov 1 (
-              primitive "move"
-              ++ brk (1,1) ++ pr.pr_name id1
-              ++ Miscprint.pr_move_location pr.pr_name id2
-            )
           | TacRename l ->
             hov 1 (
               primitive "rename" ++ brk (1,1)
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 2d5ce53075..74d98176a4 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -194,6 +194,15 @@ TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 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)) ]
+END
+
 (** Revert *)
 
 TACTIC EXTEND revert
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index e69d3f61e0..a069fd7557 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -524,8 +524,6 @@ let rec intern_atomic lf ist x =
       let h2 = intern_quantified_hypothesis ist h2 in
       TacDoubleInduction (h1,h2)
   (* Context management *)
-  | TacMove (id1,id2) ->
-    TacMove (intern_hyp ist id1,intern_move_location ist id2)
   | TacRename l ->
       TacRename (List.map (fun (id1,id2) ->
 			     intern_hyp ist id1,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 65fdecc29b..1a8a95158a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1875,11 +1875,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (TacDoubleInduction (h1,h2))
         (Elim.h_double_induction h1 h2)
   (* Context management *)
-  | TacMove (id1,id2) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1)
-                   (interp_move_location ist (pf_env gl) (project gl) id2))
-      end }
   | TacRename l ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = pf_env gl in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index ba9a74d05a..3f103a290d 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -166,7 +166,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDoubleInduction (h1,h2) as x -> x
 
   (* Context management *)
-  | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x
 
   (* Conversion *)