Module Ltac_plugin.G_auto

val wit_hyp : (Names.lident, Names.lident, Names.Id.t) Genarg.genarg_type
val __coq_plugin_name : string
val pr_hintbases : 'a -> 'b -> 'c -> string list option -> Pp.t
val wit_hintbases : (string list option, string list option, string list option) Genarg.genarg_type
val hintbases : string list option Pcoq.Entry.t
val eval_uconstrs : Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr list -> (Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr) list
val pr_auto_using_raw : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Constrexpr.constr_expr list -> Pp.t
val pr_auto_using_glob : Environ.env -> 'a -> 'b -> 'c -> 'd -> ('e Glob_term.glob_constr_g * 'f) list -> Pp.t
val pr_auto_using : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Ltac_pretype.closed_glob_constr list -> Pp.t
val wit_auto_using : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, Ltac_pretype.closed_glob_constr list) Genarg.genarg_type
val auto_using : Constrexpr.constr_expr list Pcoq.Entry.t
val make_depth : int option -> int
val deprecated_convert_concl_no_check : ?⁠loc:Loc.t -> unit -> unit
val pr_pre_hints_path_atom : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_atom_gen -> Pp.t
val pr_hints_path_atom : 'a -> 'b -> 'c -> Names.GlobRef.t Hints.hints_path_atom_gen -> Pp.t
val glob_hints_path_atom : 'a -> Libnames.qualid Hints.hints_path_atom_gen -> Names.GlobRef.t Hints.hints_path_atom_gen
val 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_type
val hints_path_atom : Libnames.qualid Hints.hints_path_atom_gen Pcoq.Entry.t
val pr_hints_path : 'a -> 'b -> 'c -> Hints.hints_path -> Pp.t
val pr_pre_hints_path : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_gen -> Pp.t
val glob_hints_path : 'a -> Libnames.qualid Hints.hints_path_gen -> Names.GlobRef.t Hints.hints_path_gen
val wit_hints_path : (Libnames.qualid Hints.hints_path_gen, Hints.hints_path, Hints.hints_path) Genarg.genarg_type
val hints_path : Libnames.qualid Hints.hints_path_gen Pcoq.Entry.t
val wit_opthints : (string list option, string list option, string list option) Genarg.genarg_type
val opthints : string list option Pcoq.Entry.t