From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Mar 2010 17:57:49 +0000 (+0000)
Subject: Comparison of two applications with a different number of arguments not
X-Git-Tag: make_still_working~3006
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=509151febaf7817e5b6ac4bd22a3d9ffa1d9a1be;hp=3dadfa509ace9184e5cf33a46d44c48c6fbed31b;p=helm.git

Comparison of two applications with a different number of arguments not
implemented yet.
---

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