From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Oct 2006 09:19:19 +0000 (+0000)
Subject: Bug fixed: inductive types were no longer removed from the environment during
X-Git-Tag: 0.4.95@7852~831
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04e808fe2e4a18c868af334ad4a2c95b0040e58d;p=helm.git

Bug fixed: inductive types were no longer removed from the environment during
a remove_single_obj.
---

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a3429840b..5e8ddaf6d 100644
--- a/components/library/librarySync.ml
+++ b/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 ***)