]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/library/librarySync.ml
moved coercion to library (work in progress)
[helm.git] / helm / ocaml / library / librarySync.ml
index 4aa9669472aba78437c4d48852e5e61d831f3402..db5239454f06dc60e109eb524dd375a44b3e0ba6 100644 (file)
@@ -220,8 +220,10 @@ let add_obj uri obj ~basedir =
 let remove_obj uri =
  let uris =
   try
-   UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri
+   let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
+    UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
+    res
   with
-   Not_found -> []
+   Not_found -> assert false
  in
   List.iter remove_single_obj (uri::uris)