set_metasenv : Cic.metasenv -> unit ;
context: Cic.context ;
set_context : Cic.context -> unit >
- (* output messages *)
- val output_html : Ui_logger.html_msg -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+ val mqi_handle : MQIConn.handle
+ val dbd:Mysql.dbd
end
module type Tactics =
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit
+ val auto : unit -> unit
end
module Make (C : Callbacks) : Tactics