From 0599dc10a00ebfe65ca64c75d0fc82723f9191a0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 11 Jul 2005 08:52:46 +0000 Subject: [PATCH] aliases are now compared not only looking at the domain_item but also looking at the description --- helm/matita/matitaSync.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 29e19c690..f42dad769 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -34,7 +34,16 @@ let alias_diff ~from status = if not (Map.mem domain_item from.aliases) then Map.add domain_item codomain_item acc else - acc) + 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 + with Not_found -> acc + end) status.aliases Map.empty let set_proof_aliases status aliases = -- 2.39.2