| NAuto (_,(None,flgs)) ->
"nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
- | NAuto (_,(Some l,flgs)) ->
+ | NAuto (_,(Some (_,l),flgs)) ->
"nautobatch" ^ " by " ^
(String.concat "," (List.map (NotationPp.pp_term status) l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
->
let l = match l with
| None -> None
- | Some _,l' -> Some (List.map (fun x -> "",0,x) l')
+ | Some (_,l') -> Some (List.map (fun x -> "",0,x) l')
in
let trace_ref = ref [] in
let status = NnAuto.auto_tac ~params:(l,a) ~trace_ref status in