X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.mli;h=86820aafbc4abaf266b1ce07e938720cc49d9f87;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=20f618f8d2bcd783c481cae5c951aedd36d5231a;hpb=26c3b57c2142bfd2242571109374c3203c7980dd;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 20f618f8d..86820aafb 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -25,13 +25,17 @@
 
 
 
-val index_obj: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+val index_obj: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
     
 (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
 
   (** 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 clean: dbd:HMysql.dbd -> string list
 
-val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+val unindex: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
 
+val count_distinct: 
+  [`Conclusion | `Hypothesis | `Statement ] -> 
+  MetadataTypes.metadata list ->
+  int