From 03b0c585e2b4946be6c529eb3359c3715ea312cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 9 Nov 2014 21:10:17 +0100
Subject: Removing the unused boolean flag from the move tactic implementation.

---
 tactics/tacinterp.ml | 2 +-
 tactics/tactics.ml   | 6 +++---
 tactics/tactics.mli  | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index feebfa40f..e16b9973f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2027,7 +2027,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end
   | TacMove (id1,id2) ->
       Proofview.V82.tactic begin fun gl -> 
-        Tactics.move_hyp true (interp_hyp ist (pf_env gl) (project gl) id1)
+        Tactics.move_hyp (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/tactics.ml b/tactics/tactics.ml
index d1ab3cb38..f8d8b09d7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -254,7 +254,7 @@ let apply_clear_request clear_flag dft c =
   else Tacticals.New.tclIDTAC
 
 (* Moving hypotheses *)
-let move_hyp        = Tacmach.move_hyp
+let move_hyp id dest gl = Tacmach.move_hyp true id dest gl
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
@@ -730,7 +730,7 @@ 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 true id dest); tac id]
+     Proofview.V82.tactic (move_hyp id dest); tac id]
     
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   Proofview.Goal.enter begin fun gl ->
@@ -817,7 +817,7 @@ let rec get_next_hyp_position id = function
 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 true id next_hyp] gl
+    [thin_for_replacing [id]; Proofview.V82.of_tactic (introduction id); move_hyp id next_hyp] gl
 
 (* 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''
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c5dfeed9c..556a5a351 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 -> tactic
 
-val move_hyp      : bool -> Id.t -> Id.t move_location -> tactic
+val move_hyp      : Id.t -> Id.t move_location -> tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic
-- 
cgit v1.2.3