Module `Ltac_plugin.Rewrite`Source

TODO: document and clean me!

Sourcetype rewrite_attributes

Sourceval rewrite_attributes : rewrite_attributes Attributes.attribute

Sourcetype unary_strategy =

| Subterms
| Subterm
| Innermost
| Outermost
| Bottomup
| Topdown
| Progress
| Try
| Any
| Repeat

Sourcetype binary_strategy =

| Compose

Sourcetype nary_strategy =

| Choice

Sourcetype ('constr, 'redexpr) strategy_ast =

| StratId
| StratFail
| StratRefl
| StratUnary of unary_strategy * ('constr, 'redexpr) strategy_ast
| StratBinary of binary_strategy * ('constr, 'redexpr) strategy_ast * ('constr, 'redexpr) strategy_ast
| StratNAry of nary_strategy * ('constr, 'redexpr) strategy_ast list
| StratConstr of 'constr * bool
| StratTerms of 'constr list
| StratHints of bool * string
| StratEval of 'redexpr
| StratFold of 'constr

Sourcetype rewrite_proof =

| RewPrf of EConstr.constr * EConstr.constr
| RewCast of Constr.cast_kind

Sourcetype evars = Evd.evar_map * Evar.Set.t

Sourcetype rewrite_result_info = {

rew_car : EConstr.constr;
rew_from : EConstr.constr;
rew_to : EConstr.constr;
rew_prf : rewrite_proof;
rew_evars : evars;

}

Sourcetype rewrite_result =

| Fail
| Identity
| Success of rewrite_result_info

Sourcetype strategy

Source

val strategy_of_ast : 
  Tacinterp.interp_sign ->
  (Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast ->
  strategy

Source

val map_strategy : 
  ('a -> 'b) ->
  ('c -> 'd) ->
  ('a, 'c) strategy_ast ->
  ('b, 'd) strategy_ast

Sourceval pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('a, 'b) strategy_ast -> Pp.t

Source

val cl_rewrite_clause_strat : 
  strategy ->
  Names.Id.t option ->
  unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Source

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

Entry point for user-level "setoid_rewrite"

Source

val is_applied_rewrite_relation : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  EConstr.constr ->
  EConstr.types option

Source

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

Source

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

Source

val add_morphism_interactive : 
  rewrite_attributes ->
  Constrexpr.constr_expr ->
  Names.Id.t ->
  Declare.Proof.t

Source

val add_morphism_as_parameter : 
  rewrite_attributes ->
  Constrexpr.constr_expr ->
  Names.Id.t ->
  unit

Source

val add_morphism : 
  rewrite_attributes ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr ->
  Names.Id.t ->
  Declare.Proof.t

Source

val get_reflexive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

val get_symmetric_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

val get_transitive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

val default_morphism : 
  ((EConstr.types * EConstr.constr option) option list
   * (EConstr.types * EConstr.types option) option) ->
  EConstr.constr ->
  EConstr.constr * EConstr.constr

Sourceval setoid_symmetry : unit Proofview.tactic

Sourceval setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic

Sourceval setoid_reflexivity : unit Proofview.tactic

Sourceval setoid_transitivity : EConstr.constr option -> unit Proofview.tactic

Source

val apply_strategy : 
  strategy ->
  Environ.env ->
  Names.Id.Set.t ->
  EConstr.constr ->
  (bool * EConstr.constr) ->
  evars ->
  rewrite_result

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Rewrite/index.html

Module `Ltac_plugin.Rewrite`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Rewrite/index.html

Module Ltac_plugin.RewriteSource

Module `Ltac_plugin.Rewrite`Source