[Kernel] remove unerasable-optional-argument warning related to wto

src/kernel_services/analysis/wto_statement.ml

@@ -39,7 +39,7 @@ let build_wto kf =
   let init = Kernel_function.find_first_stmt kf
   and succs = fun stmt -> List.rev stmt.succs
   in
-  Scheduler.partition ?pref:None ~init ~succs
+  Scheduler.partition ~pref:(fun _ _ -> 0) ~init ~succs
 
 
 (* ********************************************************************** *)

src/libraries/utils/wto.ml

@@ -187,10 +187,9 @@ module Make(N:sig
           let element = Stack.pop state.stack in
           DFN.remove state.dfn element;
           if not (N.equal element vertex) then begin
-            let best_head = match pref with
-              (** the strict is important because we are conservative *)
-              | Some cmp when cmp best_head element < 0 -> element
-              | _ -> best_head
+            (** the strict is important because we are conservative *)
+            let best_head =
+              if pref best_head element < 0 then element else best_head
             in
             reset_SCC best_head
           end
@@ -223,7 +222,7 @@ module Make(N:sig
 
   type pref = N.t -> N.t -> int
 
-  let partition ?pref ~init ~succs =
+  let partition ~pref ~init ~succs =
     let state = {dfn = DFN.create 17; num = 0; succs;
                  stack = Stack.create () } in
     let loop,component = visit ~pref state init [] in

src/libraries/utils/wto.mli

@@ -53,11 +53,12 @@ module Make(Node:sig
   end):sig
 
   type pref = Node.t -> Node.t -> int
-  (** partial order of preference for the choice of the head of a loop *)
+  (** Partial order of preference for the choice of the head of a loop.
+      Use "(fun _ _ -> 0)" for no specific preference. *)
 
   (** Implements Bourdoncle "Efficient chaotic iteration strategies with
   widenings" algorithm to compute a WTO. *)
-  val partition: ?pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
+  val partition: pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
 
   val pretty_partition: Format.formatter -> Node.t partition -> unit
   val pretty_component: Format.formatter -> Node.t component -> unit

src/plugins/wp/StmtSemantics.ml

@@ -597,7 +597,7 @@ struct
     let next = (a.return_point,Vertex.Set.empty) in
     let wto =
       WTO.partition
-        ?pref:None (* natural loop keep the heads *)
+        ~pref:(fun _ _ -> 0) (* natural loops keep their heads *)
         ~succs:(UnrollUnnatural.G.succ g)
         ~init:here in