Release 0.5.9.

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index f7062b3abebbe2b4d95956ec6f024fd4b46dcb07..7743e3726c024f55f9213dfa26f08f0c168b4630 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -40,8 +40,7 @@ let rec eq_foterm f x y =
     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 when List.length l1 = List.length l2 -> 
-        List.for_all2 (eq_foterm f) l1 l2
+    | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
     | _ -> false
 ;;
   
@@ -404,7 +403,6 @@ 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
@@ -417,8 +415,6 @@ 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 -> XINCOMPARABLE
               | _ -> assert false
           end