exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;
-let refiner_typeof =
- ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);;
-let set_refiner_typeof f = refiner_typeof := f
-;;
-
let (===) x y = Pervasives.compare x y = 0 ;;
let uncert_exc metasenv subst context t1 t2 =
assert false)
| NCicTypeChecker.TypeCheckerFailure msg ->
prerr_endline (Lazy.force msg);
+ prerr_endline (
+ "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+ ppcontext ~metasenv ~subst context ^
+ ppmetasenv ~subst metasenv);
pp msg; assert false
in
let lty = NCicSubstitution.subst_meta lc ty in