Error message fixed (dereferencing must be done eagerly, not when the error is

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.mli

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
index 0eb018b9ddf9b5395036bf08f974b959fad2be03..a9f15244cd3bc880e481bf0420885c843193c735 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
+
 val disambiguate_term :
   context:NCic.context ->
   metasenv:NCic.metasenv -> 
@@ -21,7 +23,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 +42,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) ->