| `Auto params -> pp_auto_params ~term_pp params
;;
-let pp_ntactic ~map_unicode_to_tex = function
+let rec 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
(String.concat " " (List.map string_of_int l))
| NUnfocus _ -> "##unfocus"
| NSkip _ -> "##skip"
+ | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")"
+ | NAssumption _ -> "nassumption"
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
Printf.sprintf "coercion %s %d %d %s"
(term_pp t) arity saturations
(if do_composites then "" else "nocomposites")
+
+let pp_ncommand = function
+ | UnificationHint (_,t, n) ->
+ "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NObj (_,_)
+ | NUnivConstraint (_) -> "not supported"
+ | NQed (_) -> "nqed"
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
"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 ^ " " ^ CicNotationPp.pp_term t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
| Include (_,true,path) -> "include \"" ^ path ^ "\""
| None -> "")
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
- | NObj (_,_)
- | NUnivConstraint (_) -> "not supported"
- | NQed (_) -> "nqed"
| Pump (_) -> "not supported"
let pp_punctuation_tactical =
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
+ | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function