From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Feb 2005 15:40:15 +0000 (+0000)
Subject: reverder change. no more owner passed to the locate.
X-Git-Tag: V_0_1_0~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1bfef9d9930c9a136abe0593d8da457b4e21fc3;p=helm.git

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 b36ae5b11..67b6d115c 100644
--- 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 b240ea035..b0fe0fcd3 100644
--- 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 4e6b31b53..52bd953a9 100644
--- 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 4ae870a4f..0d32e4835 100644
--- 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 ->