G_indfun (coq-core.Funind_plugin.G

val __coq_plugin_name : string

val pr_fun_ind_using : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> ('f -> 'g -> 'e -> Pp.t) -> 'h -> ('e * 'e Tactypes.bindings) option -> Pp.t

val pr_fun_ind_using_typed : (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'b -> (Environ.env -> Evd.evar_map -> 'c * ('a * 'a Tactypes.bindings)) option -> Pp.t

val wit_fun_ind_using : (Constrexpr.constr_expr Tactypes.with_bindings option, Genintern.glob_constr_and_expr Tactypes.with_bindings option, EConstr.constr Tactypes.with_bindings Tactypes.delayed_open option) Genarg.genarg_type

val fun_ind_using : Constrexpr.constr_expr Tactypes.with_bindings option Pcoq.Entry.t

val pr_intro_as_pat : ('a -> Pp.t) -> 'a Tactypes.intro_pattern_expr CAst.t option -> Pp.t

val out_disjunctive : Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t -> Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr CAst.t

val wit_with_names : (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option, Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option, Ltac_plugin.Tacexpr.intro_pattern option) Genarg.genarg_type

val with_names : Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option Pcoq.Entry.t

val functional_induction : 'a -> EConstr.constr -> (EConstr.constr * EConstr.constr Tactypes.bindings) option -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t option -> unit Proofview.tactic

val pr_constr_comma_sequence : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> 'f -> 'g -> 'e list -> Pp.t

val wit_constr_comma_sequence' : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, EConstr.constr list) Genarg.genarg_type

val constr_comma_sequence' : Constrexpr.constr_expr list Pcoq.Entry.t

val pr_auto_using : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> 'f -> 'g -> 'e list -> Pp.t

val wit_auto_using' : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, EConstr.constr list) Genarg.genarg_type

val auto_using' : Constrexpr.constr_expr list Pcoq.Entry.t

module Vernac = Pvernac.Vernac_

module Tactic = Ltac_plugin.Pltac

val wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type

val function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Pcoq.Entry.t

val is_proof_termination_interactively_checked : ('a * Constrexpr.recursion_order_expr_r CAst.t option Vernacexpr.fix_expr_gen) list -> bool

val classify_as_Fixpoint : ('a * Vernacexpr.fixpoint_expr) list -> Vernacextend.vernac_classification

val classify_funind : ('a * Vernacexpr.fixpoint_expr) list -> Vernacextend.vernac_classification

val is_interactive : ('a * Vernacexpr.fixpoint_expr) list -> bool

val pr_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) -> Pp.t

val wit_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family, unit, unit) Genarg.genarg_type

val fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) Pcoq.Entry.t

val warning_error : Libnames.qualid list -> exn -> unit