invalidate fixed

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 9875f17f6f722b7c5674a018cba684ab378e616a..ec12c8d01c80a790fec70c836ea5efa7cc4e1d3e 100644 (file)
--- 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;
     ;;