X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=e06c043722a2f03426666e9f86950f470c12066b;hb=f4460413546165a7fabbf1e1da4cf2f5a44b26b9;hp=322279769fe453cc15dafb3852567e917dae91e9;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index 322279769..e06c04372 100644
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -25,26 +25,6 @@
 
 (* $Id$ *)
 
-let alias_diff ~from status = 
-  let module Map = DisambiguateTypes.Environment in
-  Map.fold
-    (fun domain_item codomain_item acc ->
-      let description1 = GrafiteAst.description_of_alias codomain_item in
-      try
-       let description2 = 
-          GrafiteAst.description_of_alias 
-            (Map.find domain_item from#lstatus.LexiconTypes.aliases)
-       in
-        if description1 <> description2 then
-         (domain_item,codomain_item)::acc
-        else
-          acc
-      with
-       Not_found ->
-         (domain_item,codomain_item)::acc)
-    status#lstatus.LexiconTypes.aliases []
-;;
-
 let add_aliases_for_objs status =
  List.fold_left
   (fun status nref ->
@@ -57,5 +37,6 @@ let add_aliases_for_objs status =
           GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
       ) references
     in
-     LexiconEngine.set_proof_aliases status GrafiteAst.WithPreferences new_env
+     GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
+      GrafiteAst.WithPreferences new_env
   ) status