Removing useless flag of the historical move tactic.

5 files changed, 11 insertions, 11 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b7a33cdba8..4b97c1d3f0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -233,7 +233,7 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto =
   let env = Global.env() in
   let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
     if toleft
@@ -250,7 +250,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
     | (hyp,_,_) as d :: right ->
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
-	    if with_dep && not (move_location_eq hto (MoveAfter hyp)) then
+	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
 	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
@@ -529,7 +529,7 @@ let prim_refiner r sigma goal =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
 	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp true false ([],(id,None,t),named_context_of_val sign)
+	    move_hyp false ([],(id,None,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
@@ -645,11 +645,11 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
 	  ([gl], sigma)
 
-    | Move (withdep, hfrom, hto) ->
+    | Move (hfrom, hto) ->
   	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' =
-	  move_hyp withdep toleft (left,declfrom,right) hto in
+	  move_hyp toleft (left,declfrom,right) hto in
 	let (gl,ev,sigma) = mk_goal hyps' cl in
 	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
   	  ([gl], sigma)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 613f85a731..bc3b1596bc 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -32,7 +32,7 @@ type prim_rule =
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
   | Thin of Id.t list
-  | Move of bool * Id.t * Id.t move_location
+  | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9361d48e61..dcfd4b8c11 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -24,7 +24,7 @@ type prim_rule =
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
   | Thin of Id.t list
-  | Move of bool * Id.t * Id.t move_location
+  | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 03f2fd2b44..fe648e7655 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -118,8 +118,8 @@ let refine_no_check c gl =
 let thin_no_check ids gl =
   if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
 
-let move_hyp_no_check with_dep id1 id2 gl =
-  refiner (Move (with_dep,id1,id2)) gl
+let move_hyp_no_check id1 id2 gl =
+  refiner (Move (id1,id2)) gl
 
 let mutual_fix f n others j gl =
   with_check (refiner (FixRule (f,n,others,j))) gl
@@ -133,7 +133,7 @@ let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
 let thin c             = with_check (thin_no_check c)
-let move_hyp b id id'  = with_check (move_hyp_no_check b id id')
+let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 8b95ae4273..c82d1017b0 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -97,7 +97,7 @@ val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
 val thin             : Id.t list -> tactic
-val move_hyp         : bool -> Id.t -> Id.t move_location -> tactic
+val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds