sort hint's result accordingly to the "least goal left first" principle

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 56bb93ac2134fe566e740f1c53bd8370f4bb779f..3fdecb8c5850a55f700c333557d03892354c053f 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -63,10 +63,13 @@ let signature_of_hypothesis context =
           Constr.StringSet.union set (Constr.constants_of t))
     Constr.StringSet.empty context
 
-let intersect l1 l2 =
-  let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in
-  let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in
-  Constr.StringSet.elements (Constr.StringSet.inter set1 set2)
+let intersect uris siguris =
+  let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+  let set2 =
+    List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+  in
+  let inter = Constr.StringSet.inter set1 set2 in
+  List.filter (fun s -> Constr.StringSet.mem s inter) uris
 
 let filter_uris_forward ~dbh (main, constants) uris =
   let main_uris =
@@ -130,8 +133,6 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
     end else
       filter_uris_backward ~dbh (main, other_constants) uris
   in
-prerr_endline "URIS";
-List.iter prerr_endline uris;
   let rec aux = function
     | [] -> []
     | uri :: tl ->
@@ -154,7 +155,10 @@ List.iter prerr_endline uris;
               prerr_endline ("HO APPLICATO " ^ uri);
               status' :: aux tl)
   in
-  aux uris
+  List.stable_sort
+    (fun (_, (_, goals1)) (_, (_, goals2)) ->
+      Pervasives.compare (List.length goals1) (List.length goals2))
+    (aux uris)
 
 let elim ~dbh uri =
   let constraints =