helm/gTopLevel/ring.mli

   1
   2   (* ring tactics *)
   3 val ring_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status
   4
   5   (* auxiliary tactics *)
   6 val elim_type_tac:
   7   status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
   8 val reflexivity_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status
   9
  10   (* pseudo tacticals *)
  11 val try_tactics:
  12   tactics: (string * ProofEngineTypes.tactic) list ->
  13   status: ProofEngineTypes.status ->
  14   ProofEngineTypes.status
  15