diff options
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 2c57cb811e..36863906ea 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) |