Module `Ltac_plugin.G_rewrite`Source

Sourcetype constr_expr_with_bindings = Constrexpr.constr_expr Tactypes.with_bindings

type glob_constr_with_bindings =
  Genintern.glob_constr_and_expr Tactypes.with_bindings

Source

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

Source

val pr_glob_constr_with_bindings_sign : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  glob_constr_with_bindings_sign ->
  Pp.t

Source

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

Source

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

Sourceval interp_glob_constr_with_bindings : 'a -> 'b -> 'c -> 'd -> 'a * 'd

Source

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

Source

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

Source

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

Source

val glob_constr_with_bindings : 
  Constrexpr.constr_expr Tactypes.with_bindings Pcoq.Entry.t

Source

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

Source

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

Source

val interp_strategy : 
  Tacinterp.interp_sign ->
  'a ->
  'b ->
  (Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) Rewrite.strategy_ast ->
  Rewrite.strategy

Source

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

Sourceval subst_strategy : 'a -> 'b -> 'b

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

Source

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

Source

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

Source

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

Sourceval rewstrategy : raw_strategy Pcoq.Entry.t

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

Source

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

Source

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

Source

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

Source

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

Sourcetype binders_argtype = Constrexpr.local_binder_expr list

Sourceval wit_binders : binders_argtype Genarg.uniform_genarg_type

Sourceval binders : binders_argtype Pcoq.Entry.t

Source

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

Sourceval morphism_tactic : unit Proofview.tactic

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_rewrite/index.html

Module `Ltac_plugin.G_rewrite`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_rewrite/index.html

Module Ltac_plugin.G_rewriteSource

Module `Ltac_plugin.G_rewrite`Source