val disambiguate_db = initial_status
method disambiguate_db = disambiguate_db
method set_disambiguate_db v = {< disambiguate_db = v >}
val disambiguate_db = initial_status
method disambiguate_db = disambiguate_db
method set_disambiguate_db v = {< disambiguate_db = v >}
let newast, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
let newast, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
in
let _,_,thing' = thing in
let diff = diff_term Stdpp.dummy_loc thing' newast in
in
let _,_,thing' = thing in
let diff = diff_term Stdpp.dummy_loc thing' newast in
in
metasenv, subst, status, cic
;;
in
metasenv, subst, status, cic
;;
~description_of_alias:GrafiteAst.description_of_alias
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance ~uri
~description_of_alias:GrafiteAst.description_of_alias
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance ~uri