From 233836d11a41951f0197523c75a317d1070d7c6e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Apr 2008 12:03:34 +0000
Subject: [PATCH] invalidate fixed

---
 helm/software/components/cic_proof_checking/cicEnvironment.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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;
     ;;
-- 
2.39.2