From 5cf7c46b912c23461f94d83feda522527388a0d4 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Mon, 2 May 2022 09:53:00 +0200 Subject: [PATCH] [Eva] fix warning 50 --- src/libraries/utils/wto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml index 8d71938a308..db672f0228d 100644 --- a/src/libraries/utils/wto.ml +++ b/src/libraries/utils/wto.ml @@ -314,11 +314,11 @@ module Make(N:sig (* Unmark all vertices in the loop, and, if pref is given, try to return a better head *) let rec reset_SCC best_head = - (** pop until vertex *) + (* pop until vertex *) let element = Stack.pop state.stack in DFN.remove state.dfn element; if not (N.equal element vertex) then begin - (** the strict is important because we are conservative *) + (* the strict is important because we are conservative *) let best_head = if pref best_head element < 0 then element else best_head in -- GitLab