+ | C.Match (_,_,C.Meta _,_)
+ | C.Match (_,_,C.Appl (C.Meta _ :: _),_)
+ | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+ 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))))
+ | _ ->
+ raise (RefineFailure (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))))