Module Eauto
val e_assumption : unit Proofview.tacticval registered_e_assumption : unit Proofview.tacticval e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tacticval prolog_tac : Tactypes.delayed_open_constr list -> int -> unit Proofview.tacticval gen_eauto : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tacticval eauto_with_bases : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> unit Proofview.tacticval autounfold : Hints.hint_db_name list -> Locus.clause -> unit Proofview.tacticval autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tacticval autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tacticval make_dimension : int option -> int option -> bool * int