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

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 5ac709f9b..5b5b53f52 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -447,6 +447,22 @@ 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 _ =