- in
- let fail = ref ~-1 in
- let res = (try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
- in res
- (* if res then true
- else
- let relevance = get_relevance_p ~subst context _hd1 tl1 in
- let _,relevance = HExtlib.split_nth !fail relevance in
- let b,relevance = (match relevance with
- | [] -> assert false
- | b::tl -> b,tl) in
- let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
- let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
- if (not b) then
- (dance ();
- try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
- else false *)
- | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
- aux test_eq_only context hd1 hd2 &&
- let relevance = get_relevance ~subst context hd1 tl1 in
- (try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
+ in
+ let metasenv, subst, _ =
+ try
+ List.fold_left2
+ (fun (metasenv, subst, relevance) t1 t2 ->
+ let b, relevance =
+ match relevance with b::tl -> b,tl | _ -> true, [] in
+ let metasenv, subst =
+ try unify test_eq_only metasenv subst context t1 t2
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ metasenv, subst, relevance)
+ (metasenv, subst, relevance) tl1 tl2
+ with Invalid_argument _ ->
+ raise (uncert_exc metasenv subst context t1 t2)
+ in
+ metasenv, subst