helm/software/components/tactics/declarative.mli

   1 val assume : string -> Cic.term -> ProofEngineTypes.tactic
   2 val suppose : Cic.term -> string -> ProofEngineTypes.tactic
   3 val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
   4 val bydone : Cic.term -> ProofEngineTypes.tactic
   5 val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic