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

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3351725db23b5be93a1274a3ed0cf26ab6746679..3d9d74dccb76ce526869a13404e786b2fa53ea33 100644 (file)
--- 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 =