helm/gTopLevel/primitiveTactics.mli

   1 val apply_tac:
   2   term: Cic.term -> ProofEngineTypes.tactic
   3 val exact_tac:
   4   term: Cic.term -> ProofEngineTypes.tactic
   5 val intros_tac:
   6   name: string -> ProofEngineTypes.tactic
   7 val cut_tac:
   8   term: Cic.term -> ProofEngineTypes.tactic
   9 val letin_tac:
  10   term: Cic.term -> ProofEngineTypes.tactic
  11
  12 val elim_intros_simpl_tac:
  13   term: Cic.term -> ProofEngineTypes.tactic