- | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
- | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ | NAuto _ -> assert false
+ | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
+ | NRewrite (_,dir,n,where) -> "nrewrite " ^
+ (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
+ " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
+ | NDot _ -> "##."
+ | NSemicolon _ -> "##;"
+ | NBranch _ -> "##["
+ | NShift _ -> "##|"
+ | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+ | NWildcard _ -> "##*:"
+ | NMerge _ -> "##]"
+ | NFocus (_,l) ->
+ Printf.sprintf "##focus %s"
+ (String.concat " " (List.map string_of_int l))
+ | NUnfocus _ -> "##unfocus"
+ | NSkip _ -> "##skip"
+ | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
+ | NAssumption _ -> "nassumption"
+ | NBlock (_,l) ->
+ "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
+ | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t