]> matita.cs.unibo.it Git - helm.git/commitdiff
it may happen that matitaclean (clean_baseuris) calls the remove function
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Nov 2005 16:26:21 +0000 (16:26 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Nov 2005 16:26:21 +0000 (16:26 +0000)
without having added the objects first... so the hashtbl is empty...
asert fasle -> []

helm/ocaml/library/librarySync.ml

index db5239454f06dc60e109eb524dd375a44b3e0ba6..e41316ec628a5bb2714c073c6e0ad1ba791421a2 100644 (file)
@@ -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)