G_rewrite (coq-core.Ltac_plugin.G

type constr_expr_with_bindings = Constrexpr.constr_expr Tactypes.with_bindings

type glob_constr_with_bindings =
  Genintern.glob_constr_and_expr Tactypes.with_bindings

type glob_constr_with_bindings_sign =
  Geninterp.interp_sign * Genintern.glob_constr_and_expr Tactypes.with_bindings

val wit_glob_constr_with_bindings : 
  ( constr_expr_with_bindings,
    glob_constr_with_bindings,
    glob_constr_with_bindings_sign )
    Genarg.genarg_type

val glob_constr_with_bindings : constr_expr_with_bindings Pcoq.Entry.t

type raw_strategy =
  ( Constrexpr.constr_expr, Tacexpr.raw_red_expr ) Rewrite.strategy_ast

type glob_strategy =
  ( Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr )
    Rewrite.strategy_ast

val wit_rewstrategy : 
  ( raw_strategy, glob_strategy, Rewrite.strategy ) Genarg.genarg_type

val rewstrategy : raw_strategy Pcoq.Entry.t

type binders_argtype = Constrexpr.local_binder_expr list

val wit_binders : binders_argtype Genarg.uniform_genarg_type

val binders : binders_argtype Pcoq.Entry.t