...

[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 279e54b785c3903ac22d637d2af26fa7be645ce2..ae1b16f59560e745145d36009e0b22641f3e687f 100644 (file)
--- a/helm/software/components/ng_disambiguation/nDisambiguate.mli
+++ b/helm/software/components/ng_disambiguation/nDisambiguate.mli
@@ -1,17 +1,37 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
 
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
 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 *)