let pp_ntactic ~map_unicode_to_tex = function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
+ | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri
| Coercion (_, t, do_composites, i, j) ->
pp_coercion ~term_pp t do_composites i j
| PreferCoercion (_,t) ->
"prefer coercion " ^ term_pp t
+ | Inverter (_,n,ty,params) ->
+ "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris