The disambiguation now returns the aliases diff. It used to return the

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

diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index 2175a23dccebd8f651397f558b73f544f7c45f25..df5eb84b5dc01216583f9cb3fbc162d02ebe7958 100644 (file)
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -43,9 +43,6 @@ val set_proof_aliases :
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
   MatitaTypes.status
 
-val compute_diff_and_set_proof_aliases :
-  MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
-
   (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter 
    * asserts the uri is resolved to file:// so it is only for 
    * user's objects *)