X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fdisambiguate.ml;h=1e71be5b254b95738d00daf10000ddc8ae221525;hb=09151f33b14507e4d20380f3100a6db5f49f3f46;hp=afa47790ac3254173e4b2f708e8a2d570ba0d9f9;hpb=28f262128cd08dfaad435f73d3f4eee5976993d6;p=helm.git

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index afa47790a..1e71be5b2 100644
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -77,8 +77,8 @@ type domain_and_interpretation =
 module Make(C:Callbacks) =
   struct
 
-   let locate_one_id id =
-    let result = MQueryGenerator.locate id in
+   let locate_one_id mqi_handle id =
+    let result = MQueryGenerator.locate mqi_handle id in
     let uris =
      List.map
       (function uri,_ ->
@@ -121,7 +121,7 @@ module Make(C:Callbacks) =
       Uris of CicTextualParser0.uri list
     | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
 
-   let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+   let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
     let known_ids,resolve_id = id_to_uris in
     let dom' =
      let rec filter =
@@ -136,7 +136,7 @@ module Make(C:Callbacks) =
      let list_of_uris =
       List.map
        (function
-           CicTextualParser0.Id id -> Uris (locate_one_id id)
+           CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
          | CicTextualParser0.Symbol (descr,choices) ->
             (* CSC: Implementare la funzione di filtraggio manuale *)
             (* CSC: corrispondente alla locate_one_id              *)