From 64f0c19dc57a4cba968115a9f8e9ffd128580fad Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 2 Sep 2008 19:34:23 +0000
Subject: - Remove some dead code in subtac - Fix an apparent bug in the
 printing of move, indeed by default   move is _not_ dependent when parsed
 (see parsing/g_tactic.ml4).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11351 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 933667ce32..0eaac6a635 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -805,10 +805,9 @@ and pr_atom1 = function
   | TacClearBody l ->
       hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
-      (* Rem: only b = true is available for users *)
-      assert b;
       hov 1
-        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ 
+        (str "move" ++ (if b then spc () ++ str"dependent" else mt ())
+	  ++ brk (1,1) ++ pr_ident id1 ++ 
 	 pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
-- 
cgit v1.2.3