Module Ltac_plugin.G_autoSource

Sourceval __coq_plugin_name : string
Sourceval pr_hintbases : 'a -> 'b -> 'c -> string list option -> Pp.t
Sourceval wit_hintbases : (string list option, string list option, string list option) Genarg.genarg_type
Sourceval hintbases : string list option Pcoq.Entry.t
Sourceval pr_auto_using_raw : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Constrexpr.constr_expr list -> Pp.t
Sourceval pr_auto_using_glob : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> ('d Glob_term.glob_constr_g * 'e) list -> Pp.t
Sourceval pr_auto_using : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Ltac_pretype.closed_glob_constr list -> Pp.t
Sourceval make_depth : int option -> int
Sourceval deprecated_eauto_bfs : ?loc:Loc.t -> unit -> unit
Sourceval deprecated_bfs : string -> ?loc:Loc.t -> unit -> unit
Sourceval pr_pre_hints_path_atom : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_atom_gen -> Pp.t
Sourceval pr_hints_path_atom : 'a -> 'b -> 'c -> Names.GlobRef.t Hints.hints_path_atom_gen -> Pp.t
Sourceval pr_hints_path : 'a -> 'b -> 'c -> Hints.hints_path -> Pp.t
Sourceval pr_pre_hints_path : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_gen -> Pp.t
Sourceval wit_opthints : (string list option, string list option, string list option) Genarg.genarg_type
Sourceval opthints : string list option Pcoq.Entry.t