X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=0a1f1ee441e939f22e9364b1806c626db1ada685;hb=9983d0f08f594ddc01700c972d2a2c0f47d32d59;hp=4df0de08b93c5add8d741cfd17136898c56be249;hpb=a36baf354f63f6749dba7a8cc67caf3b888ba8cf;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 4df0de08b..0a1f1ee44 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -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