package coq

  1. Overview
  2. Docs
package coq
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 eq_elimination_ref : orientation -> Sorts.family -> Names.GlobRef.t option
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 Tactypes.with_bindings -> new_goals:EConstr.constr list -> unit Proofview.tactic) Hook.t
type multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
type inj_flags = {
  1. keep_proof_equalities : bool;
  2. injection_in_context : bool;
  3. injection_pattern_l2r_order : bool;
}
val discrConcl : unit Proofview.tactic
val discrHyp : Names.Id.t -> unit Proofview.tactic
val discrEverywhere : Tactics.evars_flag -> unit Proofview.tactic
exception NothingToInject
val injHyp : inj_flags option -> Tactics.clear_flag -> Names.Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> 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 -> keep_proofs:bool option -> 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