From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 26 Jun 2009 13:47:25 +0000 (+0000)
Subject: this case is not assert false since it can happen if occur_check
X-Git-Tag: make_still_working~3782
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f1f71b7b0dbb7dfaea5fd21a2c56c601269ddd4;p=helm.git

this case is not assert false since it can happen if occur_check
makes fail the unification
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6a4cc0d79..c1c0612b1 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -299,8 +299,6 @@ module Superposition (B : Terms.Blob) =
                                  footail postl, footail postr))
 			  (acc,[a],List.tl la,List.tl lb) la lb
 		      in acc
-                  | Terms.Var _, _
-                  | _, Terms.Var _ -> assert false
                   | _,_ -> None
     ;;