Eauto (coq-core.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