]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.mli
debian: rebuilt against ocaml 3.08.3
[helm.git] / helm / ocaml / metadata / metadataDb.mli
index 074ff721443aaf8e45eb31555608d7c512351123..a5b0d27534bd2146e1efc557445dfcca35757269 100644 (file)
  *)
 
   (** index a Cic.Constant object and insert resulting metadata into the db
-  * PRE_EVAL(dbh) *)
+  * PRE_EVAL(dbd) *)
 val index_constant:
-  dbh:Dbi.connection ->
-  owner:string ->
+  dbd:Mysql.dbd ->
   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 ->
-  owner:string ->
+  dbd:Mysql.dbd ->
   uri:UriManager.uri -> types:Cic.inductiveType list ->
     unit
 
 (* 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
+  (** 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 unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit