]> matita.cs.unibo.it Git - helm.git/commitdiff
CicEnvironment.remove did not remove the object from the unchecked_list.
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:09 +0000 (14:33 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:09 +0000 (14:33 +0000)
helm/ocaml/cic_proof_checking/cicEnvironment.ml

index 1f2c6be0e1704662c2c92fa46c51eb43a118c004..c111acd6cf3b75d37c7301a0a90919b02051a2c9 100644 (file)
@@ -460,7 +460,11 @@ module Cache :
      if !frozen_list <> [] then
        failwith "CicEnvironment.remove while type checking"
      else
-       HT.remove cacheOfCookedObjects uri 
+      begin
+       HT.remove cacheOfCookedObjects uri;
+       unchecked_list :=
+        List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
+      end
    ;;
    
    let  list_all_cooked_uris () =