]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: inductive types were no longer removed from the environment during
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2006 09:19:19 +0000 (09:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2006 09:19:19 +0000 (09:19 +0000)
a remove_single_obj.

helm/software/components/library/librarySync.ml

index a3429840b7b2e169c835c753529de9e4cabed0e3..5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf 100644 (file)
@@ -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 ***)