pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | 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)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NConstructor (_,None,l) -> "@ " ^
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
+ | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | 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
- | 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 _ -> "TO BE IMPLEMENTED"
| NDot _ -> "##."
| NSemicolon _ -> "##;"
let pp_nmacro = function
| NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term)
+ | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
let pp_macro ~term_pp ~lazy_term_pp =
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NInverter (_,_,_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"