X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fmatitaprover%2Fmatitaprover.ml;h=627f2604b6c2ea0c36cfc3187b4598c4d42ab999;hb=c51a6bd3e1ee41e2dc71d7829cc15e85cecea8ab;hp=b1a71034f854f9eb8ebb263ab121a7859e73b47b;hpb=18beb4339a683c5b6243673b91da878a208b36e3;p=helm.git

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index b1a71034f..627f2604b 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -110,7 +110,7 @@ let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_cla
   prerr_endline ("  " ^ oname);
   prerr_endline "Leaf order:";
   List.iter (fun ((_,name), (a,b,c,gp,l)) ->
-     prerr_endline (name ^ " " ^ string_of_int a ^ " " ^
+     prerr_endline (" " ^name ^ " " ^ string_of_int a ^ " " ^
        string_of_int b ^ " " ^
        string_of_int c ^ " " ^
        String.concat "," (List.map string_of_int gp) ^ 
@@ -163,7 +163,11 @@ end
           name, (n_occ, arity, n_gocc, g_pos, Stats.dependencies name passives))
        data
    in
-   List.sort Pervasives.compare data
+   List.sort 
+     (fun (n1,(o1,a1,go1,p1,d1)) (n2,(o2,a2,go2,p2,d2)) -> 
+        Pervasives.compare 
+          (a1,o1,go1,p1,d1) (a2,o2,go2,p2,d2))
+     data
  ;;
 
 let worker order goal hypotheses =
@@ -272,11 +276,9 @@ usage: matitaprover [options] problemfile";
     [ 
       (fun () -> worker `NRKBO goal hypotheses)
     ;
-(*
       (fun () -> worker `KBO goal hypotheses)
     ;
       (fun () -> worker `LPO goal hypotheses)
-*)
     ];
   let rec aux () =
     if List.length !childs = 0 then