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 ""
+ match univ with
+ | None -> ""
+ | Some l -> (if params <> [] then " " else "") ^ "by " ^
+ String.concat " " (List.map term_pp l)
;;
let pp_just ~term_pp =
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 "") ^
+ | NAuto (_,(None,flgs)) ->
+ "nauto" ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+ | NAuto (_,(Some l,flgs)) ->
+ "nauto" ^ " by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false