metasenv, subst
| Sys.Break -> metasenv, subst
in
- if (NCicReduction.are_convertible ~subst [] infty ty)
+ if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
then
prerr_endline ("OK: " ^ NUri.string_of_uri u)
else
NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
in*)
with
+ | Sys.Break -> ()
| NCicRefiner.RefineFailure msg
| NCicRefiner.Uncertain msg ->
let _, msg = Lazy.force msg in
prerr_endline msg;
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u))
+ prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+ | e ->
+ prerr_endline (Printexc.to_string e);
+ prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+ )
| _ -> ())
alluris;
;;