From 534a4d25a24227dac52c20d8430d12841b856350 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Dec 2008 18:07:54 +0000 Subject: [PATCH] if todo_dom was [] disambiguation was performed twice --- .../components/disambiguation/disambiguate.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index d0bf1ee17..ae56682ce 100644 --- 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 -- 2.39.2