+ let fo_unif_heads_and_cont_or_unwind_and_hints
+ test_eq_only metasenv subst m1 m2 cont hm1 hm2
+ =
+ let ms, continuation =
+ (* calling the continuation inside the outermost try is an option
+ and makes unification stronger, but looks not frequent to me
+ that heads unify but not the arguments and that an hints can fix
+ that *)
+ try fo_unif test_eq_only metasenv subst m1 m2, cont
+ with
+ | UnificationFailure _
+ | KeepReducing _ | Uncertain _ as exn ->
+ let (t1,norm1),(t2,norm2) = hm1, hm2 in
+ match
+ try_hints metasenv subst
+ (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+ with
+ | Some x -> x, fun x -> x
+ | None ->
+ match exn with
+ | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+ | UnificationFailure _ | Uncertain _ as exn -> raise exn
+ | _ -> assert false
+ in
+ continuation ms
+ in