+let alias_diff ~from status =
+ let module Map = DisambiguateTypes.Environment in
+ Map.fold_flatten
+ (fun domain_item codomain_item acc ->
+ if not (Map.mem domain_item from.aliases) then
+ Map.cons 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
+ 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
+ if DisambiguateTypes.Environment.is_empty diff then
+ new_status
+ else
+ add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
+