]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/metadataQuery.ml
locate now searched bot the standard library and the owner(user) library
[helm.git] / helm / ocaml / tactics / metadataQuery.ml
index 4df0de08b93c5add8d741cfd17136898c56be249..0a1f1ee441e939f22e9364b1806c626db1ada685 100644 (file)
@@ -49,8 +49,10 @@ let nonvar s =
 let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-        sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
+        sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
+                 "SELECT source FROM %s WHERE value LIKE \"%s\"")
           (MetadataTypes.name_tbl ()) sql_pat
+           MetadataTypes.library_name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar