raise (Uncertain (lazy (localise orig_he, Printf.sprintf
("The term %s is here applied to %d arguments but expects " ^^
"only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
- (List.length args + List.length args_so_far)
- (List.length args_so_far))))
+ (List.length args) (List.length args_so_far))))
| ty ->
let metasenv, subst, newhead, newheadty =
too_many_args := true;