+let disambiguate_nterm expty lexicon_status context metasenv subst thing
+=
+ let diff, metasenv, subst, cic =
+ singleton "first"
+ (NCicDisambiguate.disambiguate_term
+ ~coercion_db:(NCicCoercion.db ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~expty
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~lookup_in_library
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~context ~metasenv ~subst thing)
+ in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ metasenv, subst, lexicon_status, cic
+;;
+
+