--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 30/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+exception RefreshSequentException of exn
+exception RefreshProofException of exn
+
+module type Callbacks =
+ sig
+ (* input widgets *)
+ val sequent_viewer : unit -> TermViewer.sequent_viewer
+ val term_editor : unit -> TermEditor.term_editor
+ val scratch_window :
+ 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
+ end
+
+module type Tactics =
+ sig
+ val intros : 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 : ?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 : ?term:string -> unit -> unit
+ val ring : unit -> unit
+ val clearbody : unit -> unit
+ val clear : unit -> unit
+ val fourier : 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 : ?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 : ?term:string -> unit -> unit
+ val contradiction : 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
+