Removing a unused boolean in the TacMove node of tacexpr AST.

7 files changed, 10 insertions, 12 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 816502c1e5..02becc4967 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -387,8 +387,8 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacClearBody l ->
       let l = mlexpr_of_list (mlexpr_of_hyp) l in
       <:expr< Tacexpr.TacClearBody $l$ >>
-  | Tacexpr.TacMove (dep,id1,id2) ->
-      <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$
+  | Tacexpr.TacMove (id1,id2) ->
+      <:expr< Tacexpr.TacMove
               $mlexpr_of_hyp id1$
               $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7844f74e2b..efe62f569c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
   (* Context management *)
   | TacClear of bool * 'nam list
   | TacClearBody of 'nam list
-  | TacMove of bool * 'nam * 'nam move_location
+  | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
   (* Trmuctors *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e6f2af32ba..3b01e988af 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -632,7 +632,7 @@ GEXTEND Gram
         TacAtom (!@loc, TacClear (is_empty, l))
       | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l)
       | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
-	  TacAtom (!@loc, TacMove (true,hfrom,hto))
+	  TacAtom (!@loc, TacMove (hfrom,hto))
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
 
       (* Constructors *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44f4b456cc..9c9bba45b7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -879,9 +879,7 @@ module Make
               keyword "clearbody" ++ spc ()
               ++ prlist_with_sep spc pr.pr_name l
             )
-          | TacMove (b,id1,id2) ->
-            (* Rem: only b = true is available for users *)
-            assert b;
+          | TacMove (id1,id2) ->
             hov 1 (
               keyword "move"
               ++ brk (1,1) ++ pr.pr_name id1
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 9ca8da9d35..f3c7680b01 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -513,8 +513,8 @@ let rec intern_atomic lf ist x =
   (* Context management *)
   | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l)
   | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l)
-  | TacMove (dep,id1,id2) ->
-    TacMove (dep,intern_hyp ist id1,intern_move_location ist id2)
+  | 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 b320e9bb16..feebfa40f6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2025,9 +2025,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (TacClearBody l)
           (Tactics.clear_body l)
       end
-  | TacMove (dep,id1,id2) ->
+  | TacMove (id1,id2) ->
       Proofview.V82.tactic begin fun gl -> 
-        Tactics.move_hyp dep (interp_hyp ist (pf_env gl) (project gl) id1)
+        Tactics.move_hyp true (interp_hyp ist (pf_env gl) (project gl) id1)
                    (interp_move_location ist (pf_env gl) (project gl) id2)
                    gl
       end
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 1eec2f257e..2f47b90002 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -185,7 +185,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Context management *)
   | TacClear _ as x -> x
   | TacClearBody l as x -> x
-  | TacMove (dep,id1,id2) as x -> x
+  | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x
 
   (* Constructors *)