X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=92999a49e3fd687869a76b499f7ceee45a5918a0;hb=2034db684e1d295527afad07a94f2f3b6b4ed7e2;hp=96ec76013551e461c898863cd28dd7df17f0af64;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 96ec76013..92999a49e 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -116,11 +116,9 @@ let add_aliases_for_object status uri =
   
 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