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
   9
  10   (* pseudo tacticals *)
  11 val try_tactics:
  12   tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
  13 val thens:
  14  start: ProofEngineTypes.tactic ->
  15  continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
  16 val then_:
  17  start: ProofEngineTypes.tactic ->
  18  continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic