Useless "let module" removed.

[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 7f9046eb3519f168abe6a58cf999493f7b169aa7..f8a74014ae347f8802e5f2c0b489d347cdade90b 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -122,13 +122,13 @@ let report_error s =  prerr_endline (string_of_int (Unix.getpid())^": "^s);;
 
 module Main(P : Paramod.Paramod with type t = leaf) = struct
 
- let run ~useage stats goal hypotheses pp_unit_clause name = 
+ let run ~useage ~printmsg stats goal hypotheses pp_unit_clause name = 
    let bag = Terms.empty_bag, 0 in
    let bag, g_passives = P.mk_goal bag goal in
    let bag, passives = 
      HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
    in
-   start_msg stats passives g_passives pp_unit_clause name;
+   if printmsg then start_msg stats passives g_passives pp_unit_clause name;
    match
      P.paramod ~useage
       ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
@@ -181,7 +181,7 @@ end
      data
  ;;
 
-let worker order ~useage goal hypotheses =
+let worker order ~useage ~printmsg goal hypotheses =
    let stats = compute_stats goal hypotheses in
    let module C = 
      struct
@@ -212,19 +212,19 @@ let worker order ~useage goal hypotheses =
    | `NRKBO ->
        let module O = Orderings.NRKBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
    | `KBO ->
        let module O = Orderings.KBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
    | `LPO ->
        let module O = Orderings.LPO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
 ;;
 
 let print_status p = 
-  let print_endline s = prerr_endline (string_of_int p ^ ": " ^ s) in
+  let print_endline s = () in (* prerr_endline (string_of_int p ^ ": " ^ s) in*)
     function
     | Unix.WEXITED 0 -> 
         print_endline ("status Unsatisfiable for " ^ 
@@ -285,13 +285,13 @@ usage: matitaprover [options] problemfile";
          let pid = Unix.fork () in 
          if pid = 0 then (exit (f ())) else pid)
     [ 
-      (fun () -> worker `NRKBO ~useage:true goal hypotheses)
+      (fun () -> worker `NRKBO ~useage:true ~printmsg:true goal hypotheses)
     ;
-      (fun () -> worker `KBO ~useage:true goal hypotheses)
+      (fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `LPO ~useage:true goal hypotheses)
+      (fun () -> worker `LPO ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `NRKBO ~useage:false goal hypotheses)
+      (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
     ];
   let rec aux () =
     if List.length !childs = 0 then