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