From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 14 Nov 2011 15:12:57 +0000 (+0000)
Subject: Assert false is no longer true due to tooflex filtering.
X-Git-Tag: make_still_working~2118
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2781ed1b2ede944564846116e6d6b7336b75cf49;p=helm.git

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