From: denes Date: Thu, 2 Jul 2009 14:29:01 +0000 (+0000) Subject: Corrected type for bag X-Git-Tag: make_still_working~3755 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b69275324ae2d436f2f4dbb70e0ddcbdf3886636;p=helm.git Corrected type for bag --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 776d0adbb..35d6fd79c 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -85,8 +85,9 @@ let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) = Filename.basename !problem_file); flush stdout; List.iter (fun x -> + let (cl,_,_) = Terms.get_from_bag x bag in print_endline (pp ~margin:max_int - (fst(Terms.get_from_bag x bag)))) l; + cl)) l; print_endline ("% SZS output end CNFRefutation for " ^ Filename.basename !problem_file) ;;