G_auto (coq-core.Ltac_plugin.G

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 ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  ('d Glob_term.glob_constr_g * 'e) 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 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