-let add_metadata new_metadata status =
- if Helm_registry.get_bool "db.nodb" then
- let metadata = status.metadata in
- let metadata' =
- List.fold_left
- (fun acc m ->
- match m with
- | LibraryNoDb.Dependency buri ->
- if List.exists (LibraryNoDb.eq_metadata m) metadata
- then acc
- else m :: acc)
- metadata new_metadata
- in
- { status with metadata = metadata' }
- else
- status
-
-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