reverder change. no more owner passed to the locate.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b36ae5b119ecba762c529f79baeb52181f987fb8..67b6d115c2cd908daac51084287ce958be60f0c6 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -421,8 +421,8 @@ let domain_diff dom1 dom2 =
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_id ?owner dbd id =
-      let uris = MetadataQuery.locate ?owner ~dbd id in
+    let choices_of_id dbd id =
+      let uris = MetadataQuery.locate ~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) ?owner ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~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 ?owner dbd id in
+                let choices = choices_of_id dbd id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index b240ea035cac68adb1a9874a8878135e999d1e37..b0fe0fcd3e7dfa11f4a874d998971b198f2f14d2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -37,7 +37,6 @@ module Make (C : Callbacks) :
       Cic.metasenv ->
       CicAst.term ->
       ?initial_ugraph:CicUniv.universe_graph -> 
-      ?owner:string ->  
       aliases:environment ->  (* previous interpretation status *)
       (environment *                   (* new interpretation status *)
        Cic.metasenv *                  (* new metasenv *)

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 4e6b31b537ce880232b591cccc3f9197bd8726dc..52bd953a9c842e80da3ef6f4045142f6ec7e9251 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -46,23 +46,11 @@ let nonvar s =
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    match owner with
-    | None -> 
         sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
           MetadataTypes.name_tbl sql_pat
-    | Some owner -> 
-        sprintf "SELECT %s.source FROM %s,%s WHERE 
-                  (%s.source LIKE CONCAT(%s.source,\"#%%\") OR 
-                   %s.source = %s.source) AND
-                  value LIKE \"%s\" AND owner = \"%s\""
-          MetadataTypes.name_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          sql_pat owner
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar

diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index 4ae870a4f4e484c2e6eb19665809f32ae514ddfc..0d32e4835c39ec8442b75bf88e826aa08e7778bd 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.mli
+++ b/helm/ocaml/tactics/metadataQuery.mli
@@ -29,7 +29,7 @@
   * is interpreted as 0 or more characters and "?" as exactly one character *)
 val locate:
   dbd:Mysql.dbd ->
-  ?vars:bool -> ?owner:string -> string -> string list
+  ?vars:bool -> string -> string list
 
 val hint:
   dbd:Mysql.dbd ->