From 2781ed1b2ede944564846116e6d6b7336b75cf49 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Nov 2011 15:12:57 +0000 Subject: [PATCH] Assert false is no longer true due to tooflex filtering. --- matitaB/components/ng_paramodulation/superposition.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) ;; -- 2.39.2