X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataDb.mli;h=b1acc4cbe57165e071db893509b82e786102f8b5;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=86820aafbc4abaf266b1ce07e938720cc49d9f87;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/metadata/metadataDb.mli b/helm/software/components/metadata/metadataDb.mli index 86820aafb..b1acc4cbe 100644 --- a/helm/software/components/metadata/metadataDb.mli +++ b/helm/software/components/metadata/metadataDb.mli @@ -25,15 +25,15 @@ -val index_obj: dbd:HMysql.dbd -> uri:UriManager.uri -> unit +val index_obj: dbd:HSql.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:HMysql.dbd -> string list +val clean: dbd:HSql.dbd -> string list -val unindex: dbd:HMysql.dbd -> uri:UriManager.uri -> unit +val unindex: dbd:HSql.dbd -> uri:UriManager.uri -> unit val count_distinct: [`Conclusion | `Hypothesis | `Statement ] ->