From 509151febaf7817e5b6ac4bd22a3d9ffa1d9a1be Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Mar 2010 17:57:49 +0000 Subject: [PATCH] Comparison of two applications with a different number of arguments not implemented yet. --- helm/software/components/ng_paramodulation/orderings.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 7743e3726..024056ea2 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -403,6 +403,7 @@ module LPO (B : Terms.Blob) = struct | 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 @@ -415,6 +416,7 @@ module LPO (B : Terms.Blob) = struct if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT else XINCOMPARABLE | o -> o) + with Invalid_argument _ -> assert false) | XINCOMPARABLE -> XINCOMPARABLE | _ -> assert false end -- 2.39.2