context: Cic.context ;
set_context : Cic.context -> unit >
(* output messages *)
- val output_html : string -> unit
+ val output_html : Ui_logger.html_msg -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
- val mk_fresh_name_callback :
- Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
end
module type Tactics =