module type Callbacks =
sig
+ (* input widgets *)
val sequent_viewer : unit -> TermViewer.sequent_viewer
val term_editor : unit -> TermEditor.term_editor
- val get_current_scratch_infos :
+ val scratch_window :
unit ->
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option
- val set_current_scratch_infos :
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option -> unit
+ < sequent_viewer: TermViewer.sequent_viewer ;
+ show: unit -> unit ;
+ term: Cic.term ;
+ set_term : Cic.term -> unit ;
+ metasenv: Cic.metasenv ;
+ set_metasenv : Cic.metasenv -> unit ;
+ context: Cic.context ;
+ set_context : Cic.context -> unit >
+ (* output messages *)
+ val output_html : string -> unit
+ (* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
+ (* callbacks for user-tactics interaction *)
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 output_html : string -> unit
+ val notify_hbugs : unit -> unit
end
-module Make (C : Callbacks) :
+module type Tactics =
sig
val intros : unit -> unit
- val exact : unit -> unit
- val apply : unit -> unit
- val elimintrossimpl : unit -> unit
- val elimtype : unit -> unit
+ val exact : ?term:string -> unit -> unit
+ val apply : ?term:string -> unit -> unit
+ val elimintrossimpl : ?term:string -> unit -> unit
+ val elimtype : ?term:string -> unit -> unit
val whd : unit -> unit
val reduce : unit -> unit
val simpl : unit -> unit
- val fold_whd : unit -> unit
- val fold_reduce : unit -> unit
- val fold_simpl : unit -> unit
- val cut : unit -> unit
+ val fold_whd : ?term:string -> unit -> unit
+ val fold_reduce : ?term:string -> unit -> unit
+ val fold_simpl : ?term:string -> unit -> unit
+ val cut : ?term:string -> unit -> unit
val change : unit -> unit
- val letin : unit -> unit
+ val letin : ?term:string -> unit -> unit
val ring : unit -> unit
val clearbody : unit -> unit
val clear : unit -> unit
val fourier : unit -> unit
- val rewritesimpl : unit -> unit
- val rewritebacksimpl : unit -> unit
+ val rewritesimpl : ?term:string -> unit -> unit
+ val rewritebacksimpl : ?term:string -> unit -> unit
val replace : unit -> unit
val reflexivity : unit -> unit
val symmetry : unit -> unit
- val transitivity : unit -> unit
+ val transitivity : ?term:string -> unit -> unit
val exists : unit -> unit
val split : unit -> unit
val left : unit -> unit
val right : unit -> unit
val assumption : unit -> unit
val generalize : unit -> unit
- val absurd : unit -> unit
+ val absurd : ?term:string -> unit -> unit
val contradiction : unit -> unit
- val decompose : unit -> unit
- val whd_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val reduce_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val simpl_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
+ val decompose : ?term:string -> unit -> unit
+ val injection : ?term:string -> unit -> unit
+ val discriminate : ?term:string -> unit -> unit
+ val whd_in_scratch : unit -> unit
+ val reduce_in_scratch : unit -> unit
+ val simpl_in_scratch : unit -> unit
end
+
+module Make (C : Callbacks) : Tactics
+