diff options
Diffstat (limited to 'printing')
| -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) |