helm/gTopLevel/ring.mli

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