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 /printing | |
| parent | 293222e49ff81bc1299b3822d2a8c526ca803307 (diff) | |
Moving the "move" tactic to TACTIC EXTEND.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2c57cb811..36863906e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -892,12 +892,6 @@ module Make ) (* Context management *) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) | TacRename l -> hov 1 ( primitive "rename" ++ brk (1,1) |