X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconSync.ml;fp=matita%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=e06c043722a2f03426666e9f86950f470c12066b;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=9a5ff7633826b383ffd3a0a657b5e1e70128cf73;hpb=2a59f55f4625ebabb02aefc3cb8c8842040be554;p=helm.git

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index 9a5ff7633..e06c04372 100644
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -37,6 +37,6 @@ let add_aliases_for_objs status =
           GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
       ) references
     in
-     LexiconEngine.set_proof_aliases status ~implicit_aliases:false
+     GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
       GrafiteAst.WithPreferences new_env
   ) status