Ltac_plugin.G_auto
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