X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.mli;h=a1d7404bbe2acb7bb1a50282a640083dd3904891;hb=d6bdacb3cf305051e9e19f8b0422a33315a9279b;hp=074ff721443aaf8e45eb31555608d7c512351123;hpb=21758b512843088d19e81830d9fb121725c8a16e;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 074ff7214..a1d7404bb 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -24,18 +24,18 @@
  *)
 
   (** index a Cic.Constant object and insert resulting metadata into the db
-  * PRE_EVAL(dbh) *)
+  * PRE_EVAL(dbd) *)
 val index_constant:
-  dbh:Dbi.connection ->
+  dbd:Mysql.dbd ->
   owner:string ->
   uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
     unit
 
   (** index a Cic.InductiveDefinition object and insert resulting metadata into
   * the db
-  * PRE_EVAL(dbh) *)
+  * PRE_EVAL(dbd) *)
 val index_inductive_def:
-  dbh:Dbi.connection ->
+  dbd:Mysql.dbd ->
   owner:string ->
   uri:UriManager.uri -> types:Cic.inductiveType list ->
     unit
@@ -43,5 +43,5 @@ val index_inductive_def:
 (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
 
   (** remove from the db all metadata pertaining to a given owner *)
-val clean: dbh:Dbi.connection -> owner:string -> unit
+val clean: dbd:Mysql.dbd -> owner:string -> unit