X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fwhelp%2Fwhelp.ml;h=e1d8306cce105c1d75b5636bfec377311e056d88;hb=798e85cb6d55d80d988f91e6289e4041e95ad2e4;hp=5e63bcfc4e9078549f202193e66ca2ed91ce3081;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/whelp/whelp.ml b/helm/software/components/whelp/whelp.ml
index 5e63bcfc4..e1d8306cc 100644
--- a/helm/software/components/whelp/whelp.ml
+++ b/helm/software/components/whelp/whelp.ml
@@ -42,7 +42,7 @@ let sqlpat_of_shellglob =
           (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
             shellglob)))
 
-let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
         sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
@@ -50,12 +50,12 @@ let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
           (MetadataTypes.name_tbl ()) sql_pat
            MetadataTypes.library_name_tbl sql_pat
   in
-  let result = HMysql.exec dbd query in
+  let result = HSql.exec dbd query in
   List.filter nonvar
-    (HMysql.map result
+    (HSql.map result
       (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
 
-let match_term ~(dbd:HMysql.dbd) ty =
+let match_term ~(dbd:HSql.dbd) ty =
 (*   debug_print (lazy (CicPp.ppterm ty)); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =