diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-09 21:10:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-09 21:10:17 +0100 |
| commit | 03b0c585e2b4946be6c529eb3359c3715ea312cb (patch) | |
| tree | 8d6c62920404cf10a92dd9be1ee8b967e82543c1 | |
| parent | 2070c302639e841aae1558e8bc59cca6da099bdd (diff) | |
Removing the unused boolean flag from the move tactic implementation.
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | 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 |