type query = | Qnotask of Controller_itp.controller -> string list -> string| Qtask of Controller_itp.controller ->
Trans.naming_table ->
string list ->
stringval print_id : 'a -> Trans.naming_table -> string list -> stringval locate_id : 'a -> Trans.naming_table -> string list -> Loc.position optionval search_id :
search_both:bool ->
'a ->
Trans.naming_table ->
string list ->
stringval list_strategies : Controller_itp.controller -> (string * string) listval list_provers : Controller_itp.controller -> 'a -> stringval list_transforms : unit -> (string * Pp.formatted) listval load_strategies : Controller_itp.controller -> unitval return_prover : string -> Whyconf.config -> Whyconf.config_prover optiontype command = | Transform of string * Trans.gentrans * string list| Prove of Whyconf.config_prover * Call_provers.resource_limit| Strategies of string| Edit of Whyconf.prover| Get_ce| Bisect| Replay of bool| Clean| Mark_Obsolete| Focus_req| Unfocus_req| Locate of string| Help_message of string| Query of string| QError of string| Other of string * string listval interp :
(string * query) Wstdlib.Hstr.t ->
Controller_itp.controller ->
Session_itp.any option ->
string ->
commandval get_next_with_strategy :
st:Itp_communication.next_unproved_node_strat ->
always_send:bool ->
proved:('a -> bool) ->
children:('a -> 'a list) ->
get_parent:('a -> 'a option) ->
is_goal:('a -> bool) ->
is_pa:('a -> bool) ->
'a ->
'a option