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 =