(* 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