-let more_args_than_expected subst he context hetype' tlbody_and_type =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he context ^
- " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
- ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected")
+let more_args_than_expected
+ localization_tbl subst he context hetype' tlbody_and_type exn
+=
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst he context ^
+ " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^
+ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected")
+ in
+ enrich localization_tbl he ~f:(fun _-> msg) exn