helm/ocaml/tactics/ring.mli

   1
   2   (* ring tactics *)
   3 val ring_tac: ProofEngineTypes.tactic
   4
   5 (*Galla: spostata in variuosTactics.ml
   6   (* auxiliary tactics *)
   7 val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
   8 *)
   9
  10 (* spostata in variousTactics.ml
  11 val reflexivity_tac: ProofEngineTypes.tactic
  12 *)