- let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv''
- inferredty ty' ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ (try
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv''
+ inferredty ty' ugraph2
+ in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ with
+ exn ->
+ enrich localization_tbl t
+ ~f:(fun _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst'' te
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst'' inferredty
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst'' ty context)) exn
+ )