1 process for now

[helm.git] / helm / software / components / binaries / matitaprover / matitaprover.ml

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 776d0adbb6f252b5708e03957edac11cdc091c6e..c029cfa228317690d81e14b0978ee88191cc381d 100644 (file)
--- 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)
 ;;
@@ -196,9 +197,11 @@ usage: matitaprover [options] problemfile";
         let module M = Main(struct let cmp (a,_) (b,_) = compare a b end) in
         M.main goal hypotheses)
     ;
+(*
       (fun () ->     
         let module M = Main(struct let cmp (a,_) (b,_) = compare b a end) in
         M.main goal hypotheses)
+*)
     ];
   let rec aux () =
     if List.length !childs = 0 then