]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.ml
Release 0.5.9.
[helm.git] / helm / software / components / disambiguation / disambiguate.ml
index 5b5b53f52cd8a3b73edc64f35c7cb7670645157a..5ac709f9b82fc4e7b5e6dbe6f85fee64abc53570 100644 (file)
@@ -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 _ =