X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FbatchParser.mli;fp=helm%2FgTopLevel%2FbatchParser.mli;h=9ba49ef52b9ff80b11b1c9dfce55727b3de67dd1;hb=57f2f0152b79ad7096b72b7e3e83939d63454a88;hp=ff82e6fa057d9001dc43e4241d5e0a03df0640f1;hpb=cb5df9e3b544239848e779f3eaa542174b5c5806;p=helm.git diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index ff82e6fa0..9ba49ef52 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -37,7 +37,9 @@ val uri_pred_of_conf: bool -> string -> (string -> bool) * batch mode if possible, otherwise raises Failure above. * uri_pred is the predicate used to select which uris are tried. Per default * only constant URIs are accepted *) -val parse: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> (Cic.metasenv * Cic.term) list +val parse: + MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> + (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list (** as above, but instead of returning the parsed cic term, pretty prints it * (ignoring returned metasenv)