X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=42e8f1c404f0747552a2ffb3f2dda8b5b809457e;hb=11cefd39e89f8f7aefdf615f0d0eff35865b29c2;hp=472ab3a923016800a06053c194c4ec5c1072820a;hpb=405d288cca88e63515164a8d42d60087e305615c;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 472ab3a92..42e8f1c40 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -32,12 +32,13 @@ open MatitaTypes
 let extract_alias types uri = 
   fst(List.fold_left (
     fun (acc,i) (name, _, _, cl) -> 
-      ((name, UriManager.string_of_uriref (uri,[i]))
+      (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
       ::
       (fst(List.fold_left (
         fun (acc,j) (name,_) ->
-          (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
-        ) (acc,1) cl))),i+1
+          (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
+          (Some j))) :: acc) , j+1)
+        ) (acc,1) cl)),i+1
   ) ([],0) types)
 
 let env_of_list l env =
@@ -221,3 +222,9 @@ let alias_diff ~from status =
          acc)
     status.aliases Map.empty
 
+let remove uri =
+  let path = Http_getter.resolve' uri in
+  remove_object_from_disk uri path;
+  remove_coercion uri;
+  ignore(MatitaDb.remove_uri uri)
+