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
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 =