]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteDisambiguate.ml
coercions are there, but not heavily tested
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml
index fbbbf6e02c450e86e335459449423e6682166918..9950b4eb747ded55b256995bd108313d2a9da7ba 100644 (file)
@@ -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],_ ->