+let alias_diff ~from status =
+ let module Map = DisambiguateTypes.Environment in
+ Map.fold
+ (fun domain_item codomain_item acc ->
+ if not (Map.mem domain_item from.aliases) then
+ Map.add 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
+ with Not_found -> acc
+ end)
+ status.aliases Map.empty
+
+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
+ add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
+