helm/gTopLevel/primitiveTactics.mli

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