X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;fp=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5b5b53f52cd8a3b73edc64f35c7cb7670645157a;hb=d96386684e06473c5fbce2707052cf1732831d5c;hp=d0d7460a6b7a00902515510c5157e76ba7ba54c1;hpb=7c793c80721ff0b0a1d2898ba93721aa03aa4a98;p=helm.git diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index d0d7460a6..5b5b53f52 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -453,10 +453,11 @@ let disambiguate_thing let rec aux (aliases,acc) = function | [] -> aliases, acc | (Node (_, item,extra) as node) :: tl -> - let tl = tl @ extra in let choices = lookup_choices item in if List.length choices <> 1 then aux (aliases, acc@[node]) tl - else if Environment.mem item aliases then aux (aliases, acc) 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