From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Jul 2010 15:27:13 +0000 (+0000)
Subject: Bug fixed: nodes were copied.
X-Git-Tag: make_still_working~2855
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d96386684e06473c5fbce2707052cf1732831d5c;p=helm.git

Bug fixed: nodes were copied.
---

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