diff options
| author | Pierre-Marie Pédrot | 2016-02-29 13:32:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-29 13:52:48 +0100 |
| commit | 1397f791b1699b0f04d971465270d5b2df9a6d7f (patch) | |
| tree | 0ff9609e6a03baba58a1b1072a9c3b8b593ad6f9 /tactics | |
| parent | 293222e49ff81bc1299b3822d2a8c526ca803307 (diff) | |
Moving the "move" tactic to TACTIC EXTEND.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 9 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
4 files changed, 9 insertions, 8 deletions
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 *) |