why3 1.3.2 · OCaml Package

type transformation = string * string

type strategy = string

type node_ID = int

val root_node : node_ID

val is_root : node_ID -> bool

type global_information = {

}

type message_notification =

| Proof_error of node_ID * string
| Transf_error of bool * node_ID * string * string * Loc.position * string * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Information of string
| Task_Monitor of int * int * int
| Parse_Or_Type_Error of Loc.position * Loc.position * string
| File_Saved of string
| Error of string
| Open_File_Error of string

type node_type =

type color =

type update_info =

| Proved of bool
| Name_change of string
| Proof_status_change of Controller_itp.proof_attempt_status * bool * Call_provers.resource_limit

type notification =

| Reset_whole_tree
| New_node of node_ID * node_ID * node_type * string * bool
| Node_change of node_ID * update_info
| Remove of node_ID
| Next_Unproven_Node_Id of node_ID * node_ID
| Initialized of global_information
| Saving_needed of bool
| Saved
| Message of message_notification
| Dead of string
| Task of node_ID * string * (Loc.position * color) list * Loc.position option * string
| File_contents of string * string * Env.fformat * bool
| Source_and_ce of string * (Loc.position * color) list * Loc.position option * Env.fformat
| Ident_notif_loc of Loc.position

type next_unproved_node_strat =

type ide_request =

val print_request : Format.formatter -> ide_request -> unit

val print_msg : Format.formatter -> message_notification -> unit

val print_notify : Format.formatter -> notification -> unit

package why3