X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=bc4f651a449aa2663972ea2280def1cff3684515;hb=refs%2Fheads%2Fng_paramodulation_CNF;hp=c5db7a4e2ae8bc927c082bd1ceacfeee21afaba2;hpb=d5e373656748835ecfe33041bbb87b786446b75f;p=helm.git

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