- try fo_unif test_eq_only metasenv subst t1 t2
- with
- | UnificationFailure msg as exn ->
- (try
- unif_machines metasenv subst
- (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
- with
- | UnificationFailure _ -> raise (UnificationFailure msg)
- | Uncertain _ -> raise exn)
- | Uncertain msg as exn ->
-(*
- prerr_endline "PROBLEMA";
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
- let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in
- match
- try_hints metasenv subst
- (NCicReduction.unwind t1) (NCicReduction.unwind t2)
- with
- | Some x -> x
- | None ->
- try
- unif_machines metasenv subst (t1m, t2m)
+ try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
+ with
+ | KeepReducingThis (msg,tm1,tm2) ->
+ (try
+ unif_machines metasenv subst (tm1,tm2)