]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / metadata / metadataDb.mli
index d70ec4a347d4495f260129fe97b707ec7fa26cbb..86820aafbc4abaf266b1ce07e938720cc49d9f87 100644 (file)
 
 
 
-val index_obj: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+val index_obj: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
     
 (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
 
   (** remove from the db all metadata pertaining to a given owner
   * @return list of uris removed from the db *)
-val clean: dbd:Mysql.dbd -> string list
+val clean: dbd:HMysql.dbd -> string list
 
-val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+val unindex: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
 
 val count_distinct: 
   [`Conclusion | `Hypothesis | `Statement ] ->