diff options
| author | letouzey | 2012-10-06 10:08:48 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:48 +0000 |
| commit | 30cf9c6711df3eb583dacad3cb98158adbbf1f5f (patch) | |
| tree | dbb893378505ee744b94b4d8ef051018dac9d813 /printing/pptactic.ml | |
| parent | 3ab6c3a21f569ec684737e45200aa1b32f009214 (diff) | |
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
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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) |