Assert false is no longer true due to tooflex filtering.

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 12df50ebc19fecbf607bea82a091c13db331b1a1..09d708e731f5327e4a22ad3f8ca95d65ac7e062a 100644 (file)
--- a/matitaB/components/ng_paramodulation/superposition.ml
+++ b/matitaB/components/ng_paramodulation/superposition.ml
@@ -271,7 +271,7 @@ module Superposition (B : Orderings.Blob) =
             match build_clause bag (fun _ -> true)
               Terms.Demodulation (ctx inewside) subst id id2 pos dir
             with
-              | None -> assert false
+              | None -> (bag,[],t,id) (* see tooflex; was assert false *)
               | Some (bag,(id,_,_,_)) ->
                     (bag,subst,newside,id)
     ;;