-let set_proof_aliases status new_aliases =
- let commands_of_aliases =
- List.map
- (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
- in
- let deps_of_aliases =
- HExtlib.filter_map
- (function
- | LexiconAst.Ident_alias (_, suri) ->
- let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
- Some (LibraryNoDb.Dependency buri)
- | _ -> None)
- in
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status.aliases new_aliases in
- let multi_aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
- status.multi_aliases new_aliases in
- let new_status =
- { status with multi_aliases = multi_aliases ; aliases = aliases}
- in
- if new_aliases = [] then
- new_status