- let status =
- { add_aliases_for_object status uri obj with proof_status = No_proof}
- in
- LibrarySync.add_obj uri obj basedir;
- status
+ let lemmas = LibrarySync.add_obj uri obj basedir in
+ List.fold_left add_alias_for_constant
+ (add_aliases_for_object status uri obj) lemmas