Module Eauto

val e_assumption : unit Proofview.tactic
val e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
val gen_eauto : ?debug:Hints.debug -> ?depth:int -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
val eauto_with_bases : ?debug:Hints.debug -> ?depth:int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> unit Proofview.tactic
val autounfold : Hints.hint_db_name list -> Locus.clause -> unit Proofview.tactic
val autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic
val autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic