Module Funind_plugin.G_indfun

val __coq_plugin_name : string
val pr_fun_ind_using : 'a -> 'b -> ('a -> 'b -> 'c -> Pp.t) -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> ('c * 'c 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 -> 'b -> 'c -> 'd 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 -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> 'e -> 'c 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 -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> 'e -> 'c 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