- | Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
- | Tactical (_, tac, Some punct) ->
- pp_tactical ~lazy_term_pp ~term_pp tac
- ^ pp_tactical ~lazy_term_pp ~term_pp punct
- | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
+ | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
+ | Tactic (_, Some tac, punct) ->
+ pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac
+ ^ pp_punctuation_tactical punct
+ | Tactic (_, None, punct) ->
+ pp_punctuation_tactical punct
+ | NTactic (_,Some tac, punct) ->
+ pp_ntactic ~map_unicode_to_tex tac
+ ^ pp_punctuation_tactical punct
+ | NTactic (_,None, punct) ->
+ pp_punctuation_tactical punct
+ | NonPunctuationTactical (_, tac, punct) ->
+ pp_non_punctuation_tactical tac
+ ^ pp_punctuation_tactical punct