From 7aaa4bdaf1e376e557deeb51cf689a29cd809629 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 10 Feb 2021 09:31:40 +0100
Subject: [PATCH] [Wto] document 'pref' argument
---
src/libraries/utils/wto.mli | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/libraries/utils/wto.mli b/src/libraries/utils/wto.mli
index 1a693e0f597..6a12f1a3f84 100644
--- a/src/libraries/utils/wto.mli
+++ b/src/libraries/utils/wto.mli
@@ -54,6 +54,8 @@ module Make(Node:sig
type pref = Node.t -> Node.t -> int
(** Partial order of preference for the choice of the head of a loop.
+ [pref current_head new_candidate] must return < 0 if [new_candidate]
+ is preferred to [current_head].
Use "(fun _ _ -> 0)" for no specific preference. *)
(** Implements Bourdoncle "Efficient chaotic iteration strategies with
--
GitLab