val exact_tac:
term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
+ ?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit ->
ProofEngineTypes.tactic
val cut_tac:
val elim_intros_tac:
term: Cic.term -> ProofEngineTypes.tactic
+val elim_intros_tac:
+ term: Cic.term -> ProofEngineTypes.tactic
+
val change_tac:
what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic