package coq-core

  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 eq_elimination_ref : orientation -> Sorts.family -> Names.GlobRef.t option
val rewriteLR : EConstr.constr -> unit Proofview.tactic
val rewriteRL : 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
val general_rewrite : where:Names.Id.t option -> l2r:orientation -> Locus.occurrences -> freeze:freeze_evars_flag -> dep:dep_proof_flag -> with_evars:Tactics.evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
type multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
val replace_in_clause_maybe_by : bool option -> EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
type inj_flags = {
  1. keep_proof_equalities : bool;
  2. 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 inj : inj_flags option -> ?injection_in_context:bool -> Tactypes.intro_patterns option -> Tactics.evars_flag -> Tactics.clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val injClause : inj_flags option -> ?injection_in_context:bool -> Tactypes.intro_patterns option -> Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val injHyp : inj_flags option -> ?injection_in_context:bool -> Tactics.clear_flag -> Names.Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> ?injection_in_context:bool -> unit -> unit Proofview.tactic
val dEqThen : keep_proofs:bool option -> Tactics.evars_flag -> (int -> unit Proofview.tactic) -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val rewriteInHyp : bool -> EConstr.constr -> Names.Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
val set_keep_equality : Names.inductive -> bool -> unit
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.