X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=d2ae7f566ef8a737b54d46a8874327e36f758f11;hb=2b4ed41c3d8a105f1f9921b37e7f11160001bbe7;hp=b02ce3cc88f50456c80e0a482ef23d206787f3c2;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index b02ce3cc8..d2ae7f566 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -22,7 +22,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.status -> + rdb:#NCicCoercion.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> @@ -42,7 +42,7 @@ val disambiguate_obj : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - rdb:#NRstatus.status -> + rdb:#NCicCoercion.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type ->