From 30cf9c6711df3eb583dacad3cb98158adbbf1f5f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:48 +0000
Subject: remove useless hidden_flag in TacMutual(Co)Fix

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

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 055f08d93e..48a59be059 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -681,13 +681,11 @@ and pr_atom1 = function
       hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
-  | TacMutualFix (hidden,id,n,l) ->
-      if hidden then str "idtac" (* should caught before! *) else
+  | TacMutualFix (id,n,l) ->
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_fix_tac l)
   | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
-  | TacMutualCofix (hidden,id,l) ->
-      if hidden then str "idtac" (* should be caught before! *) else
+  | TacMutualCofix (id,l) ->
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
-- 
cgit v1.2.3