From 2f1f71b7b0dbb7dfaea5fd21a2c56c601269ddd4 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 26 Jun 2009 13:47:25 +0000
Subject: [PATCH] this case is not assert false since it can happen if
 occur_check makes fail the unification

---
 helm/software/components/ng_paramodulation/superposition.ml | 2 --
 1 file changed, 2 deletions(-)

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
     ;;
 
-- 
2.39.2