(* ring tactics *)
val ring_tac: ProofEngineTypes.tactic

  (* auxiliary tactics *)
val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val id_tac : ProofEngineTypes.tactic

  (* pseudo tacticals *)
val try_tactics:
  tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
val thens:
 start: ProofEngineTypes.tactic ->
 continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
val then_:
 start: ProofEngineTypes.tactic ->
 continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic