let pp_auto_params params status =
match params with
- | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+ | (None,flags) -> String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flags)
| (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
- String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+ String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flags)
;;
let pp_just status just =
| NSmartApply (_,_t) -> "fixme"
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
- String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+ String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) 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)
+ String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flgs)
| NCases (_,what,_where) -> "ncases " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NConstructor (_,None,l) -> "@ " ^
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
- | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
+ | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
- | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+ | NDestruct (_,_dom,_skip) -> "ndestruct ..."
| NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"