- debug_print
- (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
- (CicPp.ppterm hetype)
- (CicPp.ppterm hetype')
- (CicMetaSubst.ppmetasenv [] metasenv)
- (CicMetaSubst.ppsubst subst)));
- raise exn
-
+ enrich localization_tbl he
+ ~f:(fun _ ->
+ (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"
+ (* "\nReason: " ^ Lazy.force exn*)))) exn