matitaclean anapshot

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index df29edc3b7421049ec63eb5a4616560fbfcb07fd..42e8f1c404f0747552a2ffb3f2dda8b5b809457e 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -222,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)
+