X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5ac709f9b82fc4e7b5e6dbe6f85fee64abc53570;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=5b5b53f52cd8a3b73edc64f35c7cb7670645157a;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 5b5b53f52..5ac709f9b 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -447,22 +447,6 @@ let disambiguate_thing
             fix_instance item (Environment.find item e)
           with Not_found -> [])
    in
-
-   (* items with 1 choice are interpreted ASAP *)
-   let aliases, todo_dom = 
-     let rec aux (aliases,acc) = function 
-       | [] -> aliases, acc
-       | (Node (_, item,extra) as node) :: tl -> 
-           let choices = lookup_choices item in
-           if List.length choices <> 1 then aux (aliases, acc@[node]) tl
-           else
-           let tl = tl @ extra in
-           if Environment.mem item aliases then aux (aliases, acc) tl
-           else aux (Environment.add item (List.hd choices) aliases, acc) tl
-     in
-       aux (aliases,[]) todo_dom
-   in
-
 (*
       (* <benchmark> *)
       let _ =