From e59eeb6f0d8c8bcee12d97c6be6c1b972ba36cd5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Nov 2014 21:09:46 +0100
Subject: Removing the old rename tactic.

---
 printing/printer.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 1880d90ee9..5b88e8c98f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -697,10 +697,6 @@ let pr_prim_rule = function
       (str (if withdep then "dependent " else "") ++
 	 str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
 
-  | Rename (id1,id2) ->
-      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
-
-
 (* Backwards compatibility *)
 
 let prterm = pr_lconstr
-- 
cgit v1.2.3