Generation of auxiliary lemmas for inductive types and records moved

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 96ec76013551e461c898863cd28dd7df17f0af64..92999a49e3fd687869a76b499f7ceee45a5918a0 100644 (file)
--- 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