single INSERT on multiple tuples

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

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index a5b0d27534bd2146e1efc557445dfcca35757269..20f618f8d2bcd783c481cae5c951aedd36d5231a 100644 (file)
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -23,21 +23,10 @@
  * 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