if todo_dom was [] disambiguation was performed twice

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index d0bf1ee1751c0ea728d727217d714460cd055445..ae56682cef2adbd8fef6ca20c456af16d4e22320 100644 (file)
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -680,11 +680,14 @@ in refine_profiler.HExtlib.profile foo ()
               ) uncertain_l res_after_ok_l
   in
   let aux' aliases diff lookup_in_todo_dom todo_dom =
-   match test_env aliases todo_dom base_univ with
-    | Ok _
-    | Uncertain _ ->
-       aux aliases diff lookup_in_todo_dom todo_dom [] 
-    | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
+   if todo_dom = [] then
+     aux aliases diff lookup_in_todo_dom todo_dom [] 
+   else
+     match test_env aliases todo_dom base_univ with
+      | Ok _ 
+      | Uncertain _ ->
+         aux aliases diff lookup_in_todo_dom todo_dom [] 
+      | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
   in
     let res =
      match aux' aliases [] None todo_dom with