| Discriminate ident -> "discriminate " ^ ident
| Elim (term, using) ->
sprintf "elim " ^ pp_term term ^
- (match using with None -> "" | Some term -> "using " ^ pp_term term)
+ (match using with None -> "" | Some term -> " using " ^ pp_term term)
| ElimType term -> "elim type " ^ pp_term term
| Exact term -> "exact " ^ pp_term term
| Exists -> "exists"