package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

TODO: document and clean me!

type rewrite_attributes
val rewrite_attributes : rewrite_attributes Attributes.attribute
type unary_strategy =
  1. | Subterms
  2. | Subterm
  3. | Innermost
  4. | Outermost
  5. | Bottomup
  6. | Topdown
  7. | Progress
  8. | Try
  9. | Any
  10. | Repeat
type binary_strategy =
  1. | Compose
type nary_strategy =
  1. | Choice
type ('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
type rewrite_proof =
  1. | RewPrf of EConstr.constr * EConstr.constr
  2. | RewCast of Constr.cast_kind
type evars = Evd.evar_map * Evar.Set.t
type 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;
}
type rewrite_result =
  1. | Fail
  2. | Identity
  3. | Success of rewrite_result_info
type strategy
val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('a, 'b) strategy_ast -> Pp.t
val 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"

val is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
val add_morphism_as_parameter : rewrite_attributes -> Constrexpr.constr_expr -> Names.Id.t -> unit
val default_morphism : ((EConstr.types * EConstr.constr option) option list * (EConstr.types * EConstr.types option) option) -> EConstr.constr -> EConstr.constr * EConstr.constr
val setoid_symmetry : unit Proofview.tactic
val setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic
val setoid_reflexivity : unit Proofview.tactic
val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic
val apply_strategy : strategy -> Environ.env -> Names.Id.Set.t -> EConstr.constr -> (bool * EConstr.constr) -> evars -> rewrite_result