From: Stefano Zacchiroli Date: Mon, 25 Oct 2004 12:49:27 +0000 (+0000) Subject: added vars selection boolean on locate X-Git-Tag: V_0_0_10~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=26a58712246fab202250f3d994b3ea56c576c992;p=helm.git added vars selection boolean on locate --- diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 2a97a283f..54985ef68 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -23,7 +23,11 @@ * http://helm.cs.unibo.it/ *) -val locate: dbh:Dbi.connection -> string -> string list + (** @param vars if set variables (".var" URIs) are considered. Defaults to + * false *) +val locate: + dbh:Dbi.connection -> + ?vars:bool -> string -> string list val hint: dbh:Dbi.connection ->