package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.tactics/Rewrite/index.html

Module RewriteSource

TODO: document and clean me!

Sourcetype unary_strategy =
  1. | Subterms
  2. | Subterm
  3. | Innermost
  4. | Outermost
  5. | Bottomup
  6. | Topdown
  7. | Progress
  8. | Try
  9. | Any
  10. | Repeat
Sourcetype binary_strategy =
  1. | Compose
Sourcetype nary_strategy =
  1. | Choice
Sourcetype ('constr, 'redexpr) strategy_ast =
  1. | StratId
  2. | StratFail
  3. | StratRefl
  4. | StratUnary of unary_strategy * ('constr, 'redexpr) strategy_ast
  5. | StratBinary of binary_strategy * ('constr, 'redexpr) strategy_ast * ('constr, 'redexpr) strategy_ast
  6. | StratNAry of nary_strategy * ('constr, 'redexpr) strategy_ast list
  7. | StratConstr of 'constr * bool
  8. | StratTerms of 'constr list
  9. | StratHints of bool * string
  10. | StratEval of 'redexpr
  11. | StratFold of 'constr
Sourcetype rewrite_proof =
  1. | RewPrf of EConstr.constr * EConstr.constr
  2. | RewCast of Constr.cast_kind
Sourcetype rewrite_result_info = {
  1. rew_car : EConstr.constr;
  2. rew_from : EConstr.constr;
  3. rew_to : EConstr.constr;
  4. rew_prf : rewrite_proof;
  5. rew_evars : evars;
}
Sourcetype rewrite_result =
  1. | Fail
  2. | Identity
  3. | Success of rewrite_result_info
Sourcetype strategy
Sourceval 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
Sourceval cl_rewrite_clause_strat : strategy -> Names.Id.t option -> unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Entry point for user-level "setoid_rewrite"

Sourceval is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
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
Sourcemodule Internal : sig ... end