X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.mli;h=86820aafbc4abaf266b1ce07e938720cc49d9f87;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=672c900eb850ea3cb8e04538aeb65624aa929e86;hpb=5edfd170706c91c5d3a9d3522360b748a2dc034f;p=helm.git diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index 672c900eb..86820aafb 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -25,17 +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 + [`Conclusion | `Hypothesis | `Statement ] -> + MetadataTypes.metadata list -> + int