From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Nov 2005 16:26:21 +0000 (+0000)
Subject: it may happen that matitaclean (clean_baseuris) calls the remove function
X-Git-Tag: make_still_working~8059
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bf23558e2145bcc125102d61f1ca17643d0fd02;p=helm.git

it may happen that matitaclean (clean_baseuris) calls the remove function
without having added the objects first... so the hashtbl is empty...
asert fasle -> []
---

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index db5239454..e41316ec6 100644
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -224,6 +224,6 @@ let remove_obj uri =
     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
     res
   with
-   Not_found -> assert false
+    Not_found -> [] (*assert false*)
  in
   List.iter remove_single_obj (uri::uris)