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=1172bbb5d3438f752eb44c1fedcea6f903330892;hpb=67d5f78ad9593d51846bd6a69fca27e9a4ef0e6d;p=helm.git

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 1172bbb5d..627f2604b 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -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