X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;h=625de5c31994b08f8b6fc0c08a85c5b1c620584a;hb=4244a4d70b9ab2fece0ff5b63506f6d323cbfbe2;hp=cb971ea74b4e4bddf8a23a61754b9508721cd81a;hpb=f49a2aa0634549cc4fb44067225514ba7de46fec;p=helm.git diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index cb971ea74..625de5c31 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -68,8 +68,8 @@ let pp_proof bag ~formatter:f p = eq (string_of_rule rule); Format.fprintf f "|%d with %d dir %s))" eq1 eq2 (string_of_direction dir); - let (_, _, _, proof1),_ = Terms.M.find eq1 bag in - let (_, _, _, proof2),_ = Terms.M.find eq2 bag in + let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in + let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in Format.fprintf f "@["; aux eq1 proof1; aux eq2 proof2; @@ -120,10 +120,10 @@ let pp_unit_clause ~formatter:f c = Format.fprintf f "@]" ;; -let pp_bag ~formatter:f bag = +let pp_bag ~formatter:f (_,bag) = Format.fprintf f "@["; Terms.M.iter - (fun _ (c,d) -> pp_unit_clause ~formatter:f c; + (fun _ (c,d,_) -> pp_unit_clause ~formatter:f c; if d then Format.fprintf f " (discarded)@;" else Format.fprintf f "@;") bag; Format.fprintf f "@]"