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

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

(* spostata in variousTactics.ml
val reflexivity_tac: ProofEngineTypes.tactic
*)