(String.concat " " (List.map string_of_int l))
| NUnfocus _ -> "##unfocus"
| NSkip _ -> "##skip"
- | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")"
+ | 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
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
+ | NCoercion (_) -> "not supported"
| NQed (_) -> "nqed"
+ | NCopy (_,name,uri,map) ->
+ "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
+ String.concat " and "
+ (List.map
+ (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
+ map)
+;;
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri