X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=58a241e3fdc782511125d882e823350d5f4449fb;hb=70aa6dc959dc1d49f751c183367c3b73393c938b;hp=f82759195dae6bf5e50fbba9add0ed7fe09c09bc;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index f82759195..58a241e3f 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -138,7 +138,8 @@ let disambiguate_nterm expty estatus context metasenv subst thing
         ~context ~metasenv ~subst thing)
   in
   let estatus =
-    LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff
+    LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+     GrafiteAst.WithPreferences diff
   in
    metasenv, subst, estatus, cic
 ;;
@@ -219,7 +220,9 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~aliases:estatus#lstatus.LexiconTypes.aliases
       ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) 
       (text,prefix_len,obj)) in
-  let estatus = LexiconEngine.set_proof_aliases estatus
-  GrafiteAst.WithPreferences diff in
+  let estatus =
+   LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+    GrafiteAst.WithPreferences diff
+  in
    estatus, cic
 ;;