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 val reflexivity_tac: ProofEngineTypes.tactic
   8 val id_tac : ProofEngineTypes.tactic