X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=b86849f35a08b2508891c364748d512dee091e11;hb=0369aa83a42ed4730ed1946b02365760817f6ea2;hp=0eb018b9ddf9b5395036bf08f974b959fad2be03;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 0eb018b9d..b86849f35 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -21,7 +21,7 @@ val disambiguate_term : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - rdb:NRstatus.refiner_status -> + rdb:#NRstatus.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> @@ -40,7 +40,7 @@ val disambiguate_obj : mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'a DisambiguateTypes.Environment.t -> universe:'a list DisambiguateTypes.Environment.t option -> - rdb:NRstatus.refiner_status -> + rdb:#NRstatus.status -> lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> 'a list) ->