+
+let pp_auto_params ~term_pp (univ, params) =
+ String.concat " "
+ (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
+ if univ <> [] then
+ (if params <> [] then " " else "") ^ "by " ^
+ String.concat " " (List.map term_pp univ)
+ else ""
+;;
+
+let pp_just ~term_pp =
+ function
+ `Term term -> "exact " ^ term_pp term
+ | `Auto params -> pp_auto_params ~term_pp params
+;;
+
+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
+ | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
+ | NId _ -> "nid"
+ | NIntro (_,n) -> "#" ^ n
+ | 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
+;;