X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicEnvironment.ml;h=ec12c8d01c80a790fec70c836ea5efa7cc4e1d3e;hb=5acff80c93b3e3df4a52ff8cb9596de46f7bd924;hp=9875f17f6f722b7c5674a018cba684ab378e616a;hpb=92ff0c811f55b37004e2ee45dff0859c31857128;p=helm.git

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