3 val ring_tac: ProofEngineTypes.tactic
5 (* auxiliary tactics *)
6 val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
7 val reflexivity_tac: ProofEngineTypes.tactic
8 val id_tac : ProofEngineTypes.tactic
10 (* pseudo tacticals *)
12 tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
14 start: ProofEngineTypes.tactic ->
15 continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic