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 Pcoq.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 Pcoq.Entry.tval wit_constr_comma_sequence' : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, EConstr.constr list) Genarg.genarg_typeval constr_comma_sequence' : Constrexpr.constr_expr list Pcoq.Entry.tval wit_auto_using' : (Constrexpr.constr_expr list, Genintern.glob_constr_and_expr list, EConstr.constr list) Genarg.genarg_typeval auto_using' : Constrexpr.constr_expr list Pcoq.Entry.tval wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_typeval function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Pcoq.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) Pcoq.Entry.t