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.Id.t * Libnames.qualid * Sorts.family) Genarg.vernac_genarg_typeval fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) Procq.Entry.t