- clean no longer unregister URIs from the getter, but returns them

[helm.git] / helm / ocaml / metadata / metadataDb.mli

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 79bc82240f329ec2a092610c00fb0ff5aca19a27..17d6fc0947f4b5647e6494a0efe985d53e2d962f 100644 (file)
--- 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 -> 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