Module `Ltac_plugin.G_auto`Source

Sourceval __coq_plugin_name : string

Sourceval 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

Sourceval hintbases : string list option Pcoq.Entry.t

Source

val eval_uconstrs : 
  Geninterp.interp_sign ->
  Ltac_pretype.closed_glob_constr list ->
  (Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr) list

Source

val pr_auto_using_raw : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  Constrexpr.constr_expr list ->
  Pp.t

Source

val pr_auto_using_glob : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  ('d Glob_term.glob_constr_g * 'e) list ->
  Pp.t

Source

val pr_auto_using : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  Ltac_pretype.closed_glob_constr list ->
  Pp.t

Source

val wit_auto_using : 
  (Constrexpr.constr_expr list,
    Genintern.glob_constr_and_expr list,
    Ltac_pretype.closed_glob_constr list)
    Genarg.genarg_type

Sourceval auto_using : Constrexpr.constr_expr list Pcoq.Entry.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

Source

val pr_pre_hints_path_atom : 
  'a ->
  'b ->
  'c ->
  Libnames.qualid Hints.hints_path_atom_gen ->
  Pp.t

Source

val pr_hints_path_atom : 
  'a ->
  'b ->
  'c ->
  Names.GlobRef.t Hints.hints_path_atom_gen ->
  Pp.t

Source

val glob_hints_path_atom : 
  'a ->
  Libnames.qualid Hints.hints_path_atom_gen ->
  Names.GlobRef.t Hints.hints_path_atom_gen

Source

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

Sourceval hints_path_atom : Libnames.qualid Hints.hints_path_atom_gen Pcoq.Entry.t

Sourceval pr_hints_path : 'a -> 'b -> 'c -> Hints.hints_path -> Pp.t

Source

val pr_pre_hints_path : 
  'a ->
  'b ->
  'c ->
  Libnames.qualid Hints.hints_path_gen ->
  Pp.t

Source

val glob_hints_path : 
  'a ->
  Libnames.qualid Hints.hints_path_gen ->
  Names.GlobRef.t Hints.hints_path_gen

Source

val wit_hints_path : 
  (Libnames.qualid Hints.hints_path_gen, Hints.hints_path, Hints.hints_path)
    Genarg.genarg_type

Sourceval hints_path : Libnames.qualid Hints.hints_path_gen Pcoq.Entry.t

Source

val wit_opthints : 
  (string list option, string list option, string list option)
    Genarg.genarg_type

Sourceval opthints : string list option Pcoq.Entry.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_auto/index.html

Module `Ltac_plugin.G_auto`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_auto/index.html

Module Ltac_plugin.G_autoSource

Module `Ltac_plugin.G_auto`Source