X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=9950b4eb747ded55b256995bd108313d2a9da7ba;hb=63e7ef727ce32552106c4d8f3030fd264532fffe;hp=fbbbf6e02c450e86e335459449423e6682166918;hpb=6d80ab08869042fc89f54ab781a27045023acd6f;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index fbbbf6e02..9950b4eb7 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -582,9 +582,10 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
+           ~coercion_db:(NCicCoercion.db ())
            ~context:[] ~metasenv:[] ~subst:[]
-        ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+           ~aliases:lexicon_status.LexiconEngine.aliases
+           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
            (text,prefix_len,ty)
          with
          | [_,metasenv,subst,ty],_ ->