Eauto (u.4b72d9d53197f808b005effa2cda4f29.coq-core.8.20.1.doc.coq-core.tactics.Eauto)

Sourceval e_assumption : unit Proofview.tactic

val e_give_exact : 
  ?flags:Unification.unify_flags ->
  EConstr.constr ->
  unit Proofview.tactic

Source

val gen_eauto : 
  ?debug:Hints.debug ->
  ?depth:int ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list option ->
  unit Proofview.tactic

Source

val eauto_with_bases : 
  ?debug:Hints.debug ->
  ?depth:int ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db list ->
  unit Proofview.tactic

Source

val autounfold : 
  Hints.hint_db_name list ->
  Locus.clause ->
  unit Proofview.tactic

Source

val autounfold_tac : 
  Hints.hint_db_name list option ->
  Locus.clause ->
  unit Proofview.tactic

Source

val autounfold_one : 
  Hints.hint_db_name list ->
  Locus.hyp_location option ->
  unit Proofview.tactic