(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* tactic val vernac_e_resolve_constr : constr -> tactic val e_give_exact_constr : constr -> tactic val gen_eauto : bool -> bool * int -> constr list -> hint_db_name list option -> tactic