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

(*Galla: spostata in variuosTactics.ml
  (* auxiliary tactics *)
val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
*)

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