X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.mli;h=747844226c749bafab57af67f7b34d2abe6715b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=08ac016bf34e4cb175b1349d23b0858013d991fb;hpb=fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 08ac016bf..747844226 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -29,17 +29,17 @@ * is interpreted as 0 or more characters and "?" as exactly one character *) val signature_of_goal: - dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list val equations_for_goal: - dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list val locate: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?vars:bool -> string -> UriManager.uri list val experimental_hint: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?facts:bool -> ?signature:MetadataConstraints.term_signature -> ProofEngineTypes.status -> @@ -48,7 +48,7 @@ val experimental_hint: (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list val new_experimental_hint: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?facts:bool -> ?signature:MetadataConstraints.term_signature -> universe:UriManager.uri list -> @@ -57,12 +57,13 @@ val new_experimental_hint: ((Cic.term -> Cic.term) * (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list -val match_term: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val match_term: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list (** @param string is an uri *) -val elim: dbd:Mysql.dbd -> UriManager.uri -> UriManager.uri list +val elim: dbd:HMysql.dbd -> UriManager.uri -> UriManager.uri list -val instance: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val instance: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list -val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list +val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int) list