val wit_hintbases : (string list option, string list option, string list option) Genarg.genarg_typeval hintbases : string list option Pcoq.Entry.tval wit_auto_using : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, Ltac_pretype.closed_glob_constr list) Genarg.genarg_typeval auto_using : Constrexpr.constr_expr list Pcoq.Entry.tval wit_hints_path_atom : (Libnames.qualid Hints.hints_path_atom_gen, Names.GlobRef.t Hints.hints_path_atom_gen, Names.GlobRef.t Hints.hints_path_atom_gen) Genarg.genarg_typeval hints_path_atom : Libnames.qualid Hints.hints_path_atom_gen Pcoq.Entry.tval wit_hints_path : (Libnames.qualid Hints.hints_path_gen, Hints.hints_path, Hints.hints_path) Genarg.genarg_typeval hints_path : Libnames.qualid Hints.hints_path_gen Pcoq.Entry.tval wit_opthints : (string list option, string list option, string list option) Genarg.genarg_typeval opthints : string list option Pcoq.Entry.t