Added support for multiple disambiguation passes.

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index e12c1cd146c11506322c8c19514c8d6e1bb9209e..a77c2476101f5546acf3cb2445bb6e54f6921f04 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -29,25 +29,29 @@ open MatitaTypes
 
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
-  Map.fold
+  Map.fold_flatten
     (fun domain_item codomain_item acc ->
        if not (Map.mem domain_item from.aliases) then
-         Map.add domain_item codomain_item acc
+         Map.cons domain_item codomain_item acc
        else
          begin
            try 
-             let description1 = fst(Map.find domain_item from.aliases) in
-             let description2 = fst(Map.find domain_item status.aliases) in
-             if description1 <> description2 then
-               Map.add domain_item codomain_item acc
-             else
-               acc 
+             let codomain1 = Map.find domain_item from.aliases in
+             let codomain2 = Map.find domain_item status.aliases in
+             List.fold_right
+              (fun item env ->
+                let dsc = fst item in
+                if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then
+                  Map.cons domain_item codomain_item env
+                else
+                  env)
+              codomain2 acc
            with Not_found -> acc
          end)
     status.aliases Map.empty
 
 let set_proof_aliases status aliases =
- let new_status = {status with aliases = aliases } in
+ let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
  let textual_diff =
   if DisambiguateTypes.Environment.is_empty diff then