List.map
(fun (t,arity,arg) ->
- let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
+ let ty =
+ try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
+ with NCicTypeChecker.TypeCheckerFailure s ->
+ prerr_endline ("illtyped coercion: "^Lazy.force s);
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ assert false
+ in
let ty, metasenv, args =
NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
in