X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=716aa04d29f2c6f34e4280cfca3bdf49c2583333;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=cbf305261eb3fbdcba374c23e4b8721192fec41d;hpb=595d77eece3202a799e786ac5996b6b1e25fac6e;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index cbf305261..716aa04d2 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -229,13 +229,20 @@ module UriSet = Set.Make (OrderedUri)
 module IdSet  = Set.Make (OrderedId)
 
   (** @return l2 \ l1 *)
-let uri_list_diff l2 l1 =
+let urixstring_list_diff l2 l1 =
   let module S = UriSet in
   let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
   let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
   let diff = S.diff s2 s1 in
   S.fold (fun uri uris -> uri :: uris) diff []
 
+let uri_list_diff l2 l1 =
+  let module S = UriManager.UriSet in
+  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+  let diff = S.diff s2 s1 in
+  S.fold (fun uri uris -> uri :: uris) diff []
+
   (** @return l2 \ l1 *)
 let id_list_diff l2 l1 =
   let module S = IdSet in
@@ -248,15 +255,16 @@ let remove_coercion uri =
   CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
   
 let time_travel ~present ~past =
-  let objs_to_remove = uri_list_diff present.objects past.objects in
+  let objs_to_remove = urixstring_list_diff present.objects past.objects in
+  let coercions_to_remove = uri_list_diff present.coercions past.coercions in
   let notation_to_remove =
     id_list_diff present.notation_ids past.notation_ids
   in
   let debug_list = ref [] in
+  List.iter remove_coercion coercions_to_remove;
   List.iter
     (fun (uri,p) -> 
       MatitaMisc.safe_remove p;
-      remove_coercion uri;
       (try 
         CicEnvironment.remove_obj uri
       with CicEnvironment.Object_not_found _ ->