From 714256f7dcc68642117013dfa7b3ff8a76e468b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 22 Nov 2014 15:12:28 +0100
Subject: Removing useless flag of the historical move tactic.

---
 printing/printer.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 8a906b3f15..cda0403d97 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -696,9 +696,8 @@ let pr_prim_rule = function
   | Thin ids ->
       (str"clear "  ++ pr_sequence pr_id ids)
 
-  | Move (withdep,id1,id2) ->
-      (str (if withdep then "dependent " else "") ++
-	 str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
+  | Move (id1,id2) ->
+      (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
 
 (* Backwards compatibility *)
 
-- 
cgit v1.2.3