+ let try_hints metasenv subst t1 t2 (* exc*) =
+ let candidates =
+ NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
+ in
+ let rec cand_iter = function
+ | [] -> None (* raise exc *)
+ | (metasenv,c1,c2)::tl ->
+ try
+ let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
+ let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
+ Some (metasenv, subst)
+ with
+ UnificationFailure _ | Uncertain _ -> cand_iter tl
+ in
+ cand_iter candidates
+ in