]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
added owner support to the disambiguator (now locate finds only objects
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index aafbeb7777d85689fab91712b412761119476ed2..b36ae5b119ecba762c529f79baeb52181f987fb8 100644 (file)
@@ -421,8 +421,8 @@ let domain_diff dom1 dom2 =
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_id dbd id =
-      let uris = MetadataQuery.locate ~dbd id in
+    let choices_of_id ?owner dbd id =
+      let uris = MetadataQuery.locate ?owner ~dbd id in
       let uris =
        match uris with
         | [] ->
@@ -452,7 +452,7 @@ module Make (C: Callbacks) =
         uris
 
     let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
-      ?(initial_ugraph = CicUniv.empty_ugraph)  ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~aliases:current_env
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -477,7 +477,7 @@ module Make (C: Callbacks) =
               (try
                 Hashtbl.find id_choices id
               with Not_found ->
-                let choices = choices_of_id dbd id in
+                let choices = choices_of_id ?owner dbd id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb