From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 5 Dec 2008 18:07:54 +0000 (+0000)
Subject: if todo_dom was [] disambiguation was performed twice
X-Git-Tag: make_still_working~4454
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=534a4d25a24227dac52c20d8430d12841b856350;p=helm.git

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 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