Module Funind_plugin.G_indfunSource

Sourceval __coq_plugin_name : string
Sourceval pr_fun_ind_using : 'a -> 'b -> ('a -> 'b -> 'c -> Pp.t) -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> ('c * 'c Tactypes.bindings) option -> Pp.t
Sourceval 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
Sourceval pr_intro_as_pat : 'a -> 'b -> 'c -> 'd option -> Pp.t
Sourceval pr_constr_comma_sequence : 'a -> 'b -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> 'e -> 'c list -> Pp.t
Sourceval constr_comma_sequence' : Constrexpr.constr_expr list Pcoq.Entry.t
Sourceval pr_auto_using : 'a -> 'b -> ('a -> 'b -> 'c -> Pp.t) -> 'd -> 'e -> 'c list -> Pp.t
Sourcemodule Vernac = Pvernac.Vernac_
Sourcemodule Tactic = Ltac_plugin.Pltac
Sourceval is_proof_termination_interactively_checked : ('a * Constrexpr.recursion_order_expr_r CAst.t option Vernacexpr.fix_expr_gen) list -> bool
Sourceval classify_as_Fixpoint : ('a * Vernacexpr.fixpoint_expr) list -> Vernacextend.vernac_classification
Sourceval is_interactive : ('a * Vernacexpr.fixpoint_expr) list -> bool
Sourceval pr_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) -> Pp.t
Sourceval wit_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family, unit, unit) Genarg.genarg_type
Sourceval warning_error : Libnames.qualid list -> exn -> unit