- | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
- | NAuto (_,(l,flgs)) ->
- "nauto" ^
- (if l <> [] then (" by " ^
- (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
- String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
- | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> 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"