Funind_plugin.G_indfunval 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_typeval fun_ind_using :
Constrexpr.constr_expr Tactypes.with_bindings option Procq.Entry.tval 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,
Tactypes.intro_pattern option)
Genarg.genarg_typeval with_names :
Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option
Procq.Entry.tval wit_function_fix_definition :
Vernacexpr.fixpoint_expr Loc.located Genarg.vernac_genarg_typeval function_fix_definition :
Vernacexpr.fixpoint_expr Loc.located Procq.Entry.tval wit_fun_scheme_arg :
(Names.lident * Libnames.qualid * UnivGen.QualityOrSet.t)
Genarg.vernac_genarg_typeval fun_scheme_arg :
(Names.lident * Libnames.qualid * UnivGen.QualityOrSet.t) Procq.Entry.t