X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=b86849f35a08b2508891c364748d512dee091e11;hb=b266ed97b63400d62ab4ba6a4ebdfbc1d5b0c2bb;hp=6ae8bb036af0188747f753e5e7489049b8209136;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
index 6ae8bb036..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 ->
-  coercion_db:NCicCoercion.db ->
+  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 ->
-    coercion_db:NCicCoercion.db ->
+    rdb:#NRstatus.status ->
     lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
                        DisambiguateTypes.input_or_locate_uri_type ->
                        DisambiguateTypes.Environment.key -> 'a list) ->