X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf;hb=f64818068a077b8ca8a29ebc547cc488946cf072;hp=a3429840b7b2e169c835c753529de9e4cabed0e3;hpb=4b98f68b964c9f87868c445e794bc745a99d5b17;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index a3429840b..5e8ddaf6d 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -173,8 +173,8 @@ let remove_single_obj uri =
    (fun uri -> 
      ignore (LibraryDb.remove_uri uri);
      (*CoercGraph.remove_coercion uri;*)
-     CicEnvironment.remove_obj uri
-   ) uris_to_remove
+   ) uris_to_remove ;
+  CicEnvironment.remove_obj uri
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)