From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 17 Oct 2010 09:09:12 +0000 (+0000)
Subject: fixed List.for_all2 called without knowing if the two lists have the same length
X-Git-Tag: make_still_working~2775
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6ee1124bbfd9ecf01ed5fd5b92e0b32b2c47d97;p=helm.git

fixed List.for_all2 called without knowing if the two lists have the same length
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 1e143605b..f7062b3ab 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -40,7 +40,8 @@ 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 -> 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
 ;;