X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=09d708e731f5327e4a22ad3f8ca95d65ac7e062a;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=12df50ebc19fecbf607bea82a091c13db331b1a1;hpb=d6578d33463c053073c6dab75728ca318717e1de;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 12df50ebc..09d708e73 100644
--- 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)
     ;;