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

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 17d6fc094..d70ec4a34 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -23,24 +23,19 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** index a Cic.Constant object and insert resulting metadata into the db
-  * PRE_EVAL(dbd) *)
-val index_constant:
-  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(dbd) *)
-val index_inductive_def:
-  dbd:Mysql.dbd ->
-  uri:UriManager.uri -> types:Cic.inductiveType list ->
-    unit
 
+val index_obj: dbd:Mysql.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 unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+
+val count_distinct: 
+  [`Conclusion | `Hypothesis | `Statement ] -> 
+  MetadataTypes.metadata list ->
+  int