...

[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 1172bbb5d3438f752eb44c1fedcea6f903330892..627f2604b6c2ea0c36cfc3187b4598c4d42ab999 100644 (file)
--- 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