From d9037e385e4cb12eccd8a734f4a9fc1a5a0f8b62 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 16:16:19 +0000 Subject: [PATCH] added invalidate --- .../components/ng_kernel/nCicEnvironment.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index fcb408326..599e1691f 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -13,7 +13,7 @@ let get_checked_obj u = (* FIX: add all objects to the environment and give back the last one *) let l = OCic2NCic.convert_obj ouri o in List.iter (fun (u,_,_,_,_ as o) -> - prerr_endline ("+"^NUri.string_of_uri u); +(* prerr_endline ("+"^NUri.string_of_uri u); *) NUri.UriHash.add cache u (false,o)) l; HExtlib.list_last l ;; @@ -28,7 +28,7 @@ let get_obj u = in let l = OCic2NCic.convert_obj ouri o in List.iter (fun (u,_,_,_,_ as o) -> - prerr_endline ("+"^NUri.string_of_uri u); +(* prerr_endline ("+"^NUri.string_of_uri u); *) NUri.UriHash.add cache u (false,o)) l; false, HExtlib.list_last l ;; @@ -76,3 +76,12 @@ let get_indty_leftno = function | _,_,_,_, NCic.Inductive (_,left,_,_) -> left | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false) | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false +;; + +let invalidate _ = + List.iter + (fun (k,v) -> + NUri.UriHash.replace cache k (false,v)) + (NUri.UriHash.fold (fun k v -> (@) [k,snd v]) cache []) +;; + -- 2.39.2