Yet another implementation of the single aliases / multi aliases idea.

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 55cb4a45c09d45c887e07c26602934283bc61679..c4f8f554724a5422bed9f80c2e03a94d252727bf 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -29,23 +29,19 @@ open MatitaTypes
 
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
-  Map.fold_flatten
+  Map.fold
     (fun domain_item codomain_item acc ->
        if not (Map.mem domain_item from.aliases) then
-         Map.cons domain_item codomain_item acc
+         Map.add domain_item codomain_item acc
        else
          begin
            try 
-             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
+            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
            with Not_found -> acc
          end)
     status.aliases Map.empty
@@ -53,6 +49,10 @@ let alias_diff ~from status =
 let set_proof_aliases status aliases =
  let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
+ let multi_aliases =
+  DisambiguateTypes.Environment.fold DisambiguateTypes.Environment.cons
+   diff status.multi_aliases in
+ let new_status = { new_status with multi_aliases = multi_aliases } in
  if DisambiguateTypes.Environment.is_empty diff then
    new_status
  else