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 6a4cc0d791564d79cd317378028abf6cca97bccf..c1c0612b1e39d39c7b166357670a3fc9c180b01d 100644 (file)
--- 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
     ;;