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 pr_glob_constr_with_bindings_sign : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> glob_constr_with_bindings_sign -> Pp.t

val pr_glob_constr_with_bindings : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> glob_constr_with_bindings -> Pp.t

val pr_constr_expr_with_bindings : 'a -> 'b -> ('c -> 'd -> Constrexpr.constr_expr -> 'e) -> 'f -> 'g -> constr_expr_with_bindings -> 'h

val interp_glob_constr_with_bindings : 'a -> 'b -> 'c -> 'd -> 'e * 'f

val glob_glob_constr_with_bindings : Tacintern.glob_sign -> (Constrexpr.constr_expr * Constrexpr.constr_expr Tactypes.bindings) -> Genintern.glob_constr_and_expr * Genintern.glob_constr_and_expr Tactypes.bindings

val subst_glob_constr_with_bindings : Mod_subst.substitution -> Genintern.glob_constr_and_expr Tactypes.with_bindings -> Genintern.glob_constr_and_expr Tactypes.with_bindings

val wit_glob_constr_with_bindings : (Constrexpr.constr_expr Tactypes.with_bindings, Genintern.glob_constr_and_expr Tactypes.with_bindings, glob_constr_with_bindings_sign) Genarg.genarg_type

val glob_constr_with_bindings : Constrexpr.constr_expr Tactypes.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 interp_strategy : Tacinterp.interp_sign -> 'a -> 'b -> (Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) Rewrite.strategy_ast -> Rewrite.strategy

val glob_strategy : Tacintern.glob_sign -> (Constrexpr.constr_expr, Tacexpr.raw_red_expr) Rewrite.strategy_ast -> (Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) Rewrite.strategy_ast

val subst_strategy : 'a -> 'b -> 'c

val pr_strategy : 'a -> 'b -> 'c -> Rewrite.strategy -> Pp.t

val pr_raw_strategy : Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) -> 'a -> raw_strategy -> Pp.t

val pr_glob_strategy : Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) -> 'a -> glob_strategy -> Pp.t

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

val rewstrategy : raw_strategy Pcoq.Entry.t

val db_strat : string -> ('a, 'b) Rewrite.strategy_ast

val cl_rewrite_clause_db : 'a -> string -> Names.Id.t option -> unit Proofview.tactic

val cl_rewrite_clause : (Tacinterp.interp_sign * Genintern.glob_constr_and_expr Tactypes.with_bindings) -> bool -> Locus.occurrences -> Names.Id.t option -> unit Proofview.tactic

val clsubstitute : bool -> (Tacinterp.interp_sign * Genintern.glob_constr_and_expr Tactypes.with_bindings) -> unit Proofview.tactic

val declare_relation : ComRewrite.rewrite_attributes -> Constrexpr.constr_expr -> ?binders:Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr -> Names.Id.t CAst.t -> Constrexpr.constr_expr option -> Constrexpr.constr_expr option -> Constrexpr.constr_expr option -> unit

type binders_argtype = Constrexpr.local_binder_expr list

val wit_binders : binders_argtype Genarg.uniform_genarg_type

val binders : binders_argtype Pcoq.Entry.t

val add_setoid : ComRewrite.rewrite_attributes -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t CAst.t -> unit

val morphism_tactic : unit Proofview.tactic