val exact_tac:
term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
- name: string -> ProofEngineTypes.tactic
+ mknames: (unit -> string) -> ProofEngineTypes.tactic
val cut_tac:
term: Cic.term -> ProofEngineTypes.tactic
val letin_tac:
term: Cic.term -> ProofEngineTypes.tactic
-val elim_intros_simpl_tac:
+val elim_simpl_intros_tac:
term: Cic.term -> ProofEngineTypes.tactic
val change_tac: