prerr_endline ("start: " ^ NUri.string_of_uri u);
let bo = curryfy [] bo in
(try
+ let rdb = {
+ NRstatus.uhint_db = NCicUnifHint.empty_db;
+ NRstatus.coerc_db = NCicCoercion.empty_db;
+ NRstatus.library_db = NCicLibrary.time0;
+ NRstatus.dump = fun x -> x
+ } in
let metasenv, subst, bo, infty =
- NCicRefiner.typeof
- ~look_for_coercion:(fun _ _ _ _ _ -> [])
- NCicUnifHint.empty_db [] [] [] bo None
+ NCicRefiner.typeof rdb [] [] [] bo None
in
let metasenv, subst =
try
- NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty
+ NCicUnification.unify rdb metasenv subst [] infty ty
with
| NCicUnification.Uncertain msg
| NCicUnification.UnificationFailure msg