(* ring tactics *)
val ring_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status

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

  (* pseudo tacticals *)
val try_tactics:
  tactics: (string * ProofEngineTypes.tactic) list ->
  status: ProofEngineTypes.status ->
  ProofEngineTypes.status