let pp_ntactic ~map_unicode_to_tex = function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NId _ -> "nid"
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
^ pp_punctuation_tactical punct
| Tactic (_, None, punct) ->
pp_punctuation_tactical punct
- | NTactic (_,Some tac, punct) ->
+ | NTactic (_,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