package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type dep_proof_flag = bool
type freeze_evars_flag = bool
type orientation = bool
type conditions =
  1. | Naive
  2. | FirstSolved
  3. | AllMatches
val rewriteLR : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
val general_setoid_rewrite_clause : (Names.Id.t option -> orientation -> Locus.occurrences -> EConstr.constr Misctypes.with_bindings -> new_goals:EConstr.constr list -> unit Proofview.tactic) Hook.t
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
val discrConcl : unit Proofview.tactic
val discrHyp : Names.Id.t -> unit Proofview.tactic
val discrEverywhere : Misctypes.evars_flag -> unit Proofview.tactic
val injConcl : unit Proofview.tactic
val cutRewriteInHyp : bool -> EConstr.types -> Names.Id.t -> unit Proofview.tactic
val cutRewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
val rewriteInHyp : bool -> EConstr.constr -> Names.Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
type subst_tactic_flags = {
  1. only_leibniz : bool;
  2. rewrite_dependent_proof : bool;
}
val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
val subst : Names.Id.t list -> unit Proofview.tactic
val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
val set_eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind -> unit
OCaml

Innovation. Community. Security.