| `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
| `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
| `Match(t,(v,ar),bs_lift,bs,args) ->
- "[match("^ string_of_var v ^":"^ string_of_int ar ^") " ^ string_of_term_no_pars l (t :> nf) ^
- " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
- String.concat " " (List.map (string_of_term l) args) ^ ")"
- and string_of_term_no_pars_app l = function
- | `I((n,ar), args) -> print_name l n ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
+ "["^ string_of_var v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars l (t :> nf) ^
+ " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift (t :> nf))) !bs) ^ "] " ^
+ String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
+ and string_of_term_no_pars_app l = function
+ | `I((n,ar), args) -> print_name l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args :> nf list))
| #nf as t -> string_of_term_w_pars l t
and string_of_term_no_pars_lam l = function
| `Lam(_,t) -> let name = string_of_var (List.length l) in