val fail : ProofEngineTypes.tactic
val fold :
reduction:(Cic.context -> Cic.term -> Cic.term) ->
+ term:Cic.term ->
pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val fourier : ProofEngineTypes.tactic
-val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val fwd_simpl :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
ProofEngineTypes.pattern -> ProofEngineTypes.tactic
unit -> ProofEngineTypes.tactic
val lapply :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?how_many:int ->
+ ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val left : ProofEngineTypes.tactic
val letin :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
pattern:ProofEngineTypes.pattern ->
with_what:Cic.term -> ProofEngineTypes.tactic
val rewrite :
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back :
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl :
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val rewrite_simpl :
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
val set_goal : int -> ProofEngineTypes.tactic