diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 13:32:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 13:52:48 +0100 |
| commit | 1397f791b1699b0f04d971465270d5b2df9a6d7f (patch) | |
| tree | 0ff9609e6a03baba58a1b1072a9c3b8b593ad6f9 /tactics/tacinterp.ml | |
| parent | 293222e49ff81bc1299b3822d2a8c526ca803307 (diff) | |
Moving the "move" tactic to TACTIC EXTEND.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 65fdecc29..1a8a95158 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 |