- further simplifications (??) of the status dependencies

[helm.git] / matita / components / lexicon / lexiconSync.ml

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index 9a5ff7633826b383ffd3a0a657b5e1e70128cf73..e06c043722a2f03426666e9f86950f470c12066b 100644 (file)
--- 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