val apply_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val exact_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
- status: ProofEngineTypes.status -> name: string-> ProofEngineTypes.status
+ name: string -> ProofEngineTypes.tactic
val cut_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val letin_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val elim_intros_simpl_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic