...

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

diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.mli b/helm/software/components/ng_disambiguation/nDisambiguate.mli
index a61d37653990b25f82039e8af7d254a4c28dfc33..ae1b16f59560e745145d36009e0b22641f3e687f 100644 (file)
--- a/helm/software/components/ng_disambiguation/nDisambiguate.mli
+++ b/helm/software/components/ng_disambiguation/nDisambiguate.mli
@@ -14,15 +14,24 @@
 module Make (C : DisambiguateTypes.Callbacks) : sig
 val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:HSql.dbd ->
     context:NCic.context ->
     metasenv:NCic.metasenv ->
     subst:NCic.substitution ->
-    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
-    universe:DisambiguateTypes.multiple_environment option ->
+    aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:NCic.term DisambiguateTypes.multiple_environment option ->
+    lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+                        ?ok:string ->
+                        ?enable_button_for_non_vars:bool ->
+                        title:string ->
+                        msg:string ->
+                        id:string ->
+                        UriManager.uri list -> UriManager.uri list) ->
+                       (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+                       DisambiguateTypes.Environment.key ->
+                       NCic.term DisambiguateTypes.codomain_item list) ->
     ?goal: int ->
     CicNotationPt.term Disambiguate.disambiguator_input ->
-    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+    ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list *
      NCic.metasenv *                  (* new metasenv *)
      NCic.substitution *
      NCic.term) list *  (* disambiguated term *)