...

[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 d1175648aa866ce856897b0ddda9ebc176f1569c..b86849f35a08b2508891c364748d512dee091e11 100644 (file)
--- 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) ->
@@ -50,3 +50,5 @@ val disambiguate_obj :
      NCic.substitution * NCic.obj)
     list * bool
 
+val disambiguate_path: CicNotationPt.term -> NCic.term
+