X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=3d9d74dccb76ce526869a13404e786b2fa53ea33;hb=b12aa2f7dc56d9915603339e9a1e1ba23d834b4a;hp=3351725db23b5be93a1274a3ed0cf26ab6746679;hpb=ae3540a0dc8b1e1cccb04b811bf558fb6fff9577;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3351725db..3d9d74dcc 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -63,11 +63,6 @@ let set_proof_aliases status new_aliases =
     (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases)
     new_status
 
-let compute_diff_and_set_proof_aliases status aliases =
- let new_status = { status with aliases = aliases } in
- let diff = alias_diff ~from:status new_status in
-  set_proof_aliases status diff
-  
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate authomatic aliases **)
 let extract_alias types uri =