diff --git a/src/libraries/utils/wto.mli b/src/libraries/utils/wto.mli index 1a693e0f597fba0d8209a17f240e94ea390c4daf..6a12f1a3f847e361a9692454ed3b326f1eea29d3 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