X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.mli;h=a5b0d27534bd2146e1efc557445dfcca35757269;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=a1d7404bbe2acb7bb1a50282a640083dd3904891;hpb=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index a1d7404bb..a5b0d2753 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -27,7 +27,6 @@
   * PRE_EVAL(dbd) *)
 val index_constant:
   dbd:Mysql.dbd ->
-  owner:string ->
   uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
     unit
 
@@ -36,12 +35,14 @@ val index_constant:
   * PRE_EVAL(dbd) *)
 val index_inductive_def:
   dbd:Mysql.dbd ->
-  owner:string ->
   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: dbd:Mysql.dbd -> 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