Ltac_plugin.G_rewrite
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 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 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