Ltac_plugin.G_rewritetype constr_expr_with_bindings = Constrexpr.constr_expr Tactypes.with_bindingstype glob_constr_with_bindings = Genintern.glob_constr_and_expr Tactypes.with_bindingstype glob_constr_with_bindings_sign = Geninterp.interp_sign * Genintern.glob_constr_and_expr Tactypes.with_bindingsval wit_glob_constr_with_bindings : (constr_expr_with_bindings, glob_constr_with_bindings, glob_constr_with_bindings_sign) Genarg.genarg_typeval glob_constr_with_bindings : constr_expr_with_bindings Pcoq.Entry.tval wit_rewstrategy : (Tacexpr.raw_strategy, Tacexpr.glob_strategy, Rewrite.strategy) Genarg.genarg_typeval rewstrategy : Tacexpr.raw_strategy Pcoq.Entry.ttype binders_argtype = Constrexpr.local_binder_expr listval wit_binders : binders_argtype Genarg.uniform_genarg_typeval binders : binders_argtype Pcoq.Entry.t