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