match x, y with
| Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
| Terms.Var i, Terms.Var j -> i = j
- | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
+ | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 ->
+ List.for_all2 (eq_foterm f) l1 l2
| _ -> false
;;
| XLT -> if check_subterms t (l_ol,tl1) then XLT
else XINCOMPARABLE
| XEQ ->
+ (try
let lex = List.fold_left2
(fun acc si ti -> if acc = XEQ then lpo si ti else acc)
XEQ tl1 tl2
if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
else XINCOMPARABLE
| o -> o)
+ with Invalid_argument _ -> (* assert false *)
+ XINCOMPARABLE)
| XINCOMPARABLE -> XINCOMPARABLE
| _ -> assert false
end