Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
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 injection : unit -> unit
- val discriminate : 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
+