NCicPp.ppterm ~metasenv ~subst ~context t2);
*)
let candidates =
- NCicUnifHint.look_for_hint
- rdb.NRstatus.uhint_db metasenv subst context t1 t2
+ NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
in
let rec cand_iter = function
| [] -> None (* raise exc *)