From: denes Date: Fri, 25 Sep 2009 22:27:12 +0000 (+0000) Subject: Fixed typo X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b618c488ec6b128767af82128d1d4d953cf5c8af;p=helm.git Fixed typo --- diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index c5db7a4e2..bc4f651a4 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -280,8 +280,8 @@ module Superposition (B : Orderings.Blob) = let rec demod_lit ~jump_to_right bag id lit clause_ctx = (match lit with | Terms.Predicate t -> assert false - | Terms.Equation (l,r,ty,_) -> assert false - (*let bag,l,id1,lit = + | Terms.Equation (l,r,ty,_) -> + let bag,l,id1,lit = visit bag [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l (ctx_demod table vl clause_ctx) @@ -291,8 +291,7 @@ module Superposition (B : Orderings.Blob) = (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r (ctx_demod table vl clause_ctx) in - let cl,_,_ = Terms.get_from_bag id2 bag in - bag,id2,cl *) ) + bag,id2,lit) in let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id else List.fold_left