From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Apr 2008 12:03:34 +0000 (+0000)
Subject: invalidate fixed
X-Git-Tag: make_still_working~5384
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=233836d11a41951f0197523c75a317d1070d7c6e;p=helm.git

invalidate fixed
---

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 9875f17f6..ec12c8d01 100644
--- a/helm/software/components/cic_proof_checking/cicEnvironment.ml
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml
@@ -146,7 +146,9 @@ module Cache :
 
     let invalidate _ =
       let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in
-      unchecked_list := l ;
+      unchecked_list := 
+        HExtlib.list_uniq ~eq:(fun (x,_) (y,_) -> UriManager.eq x y)
+        (List.sort (fun (x,_) (y,_) -> UriManager.compare x y) (l @ !unchecked_list));
       frozen_list := [];
       HT.clear cacheOfCookedObjects;
     ;;