CicEnvironment.remove did not remove the object from the unchecked_list.

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 1f2c6be0e1704662c2c92fa46c51eb43a118c004..c111acd6cf3b75d37c7301a0a90919b02051a2c9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -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 () =