let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in
- 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
let add_obj =
let profiler = HExtlib.profile "add_obj" in