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

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index a1d7404bb..17d6fc094 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,12 @@ 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