package coq-core

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

Install 

dune-project
 Dependency

coq.inria.fr 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/Equality/index.html

Module EqualitySource

Sourcetype dep_proof_flag = bool
Sourcetype freeze_evars_flag = bool
Sourcetype orientation = bool
Sourcetype conditions =
  1. | Naive
  2. | FirstSolved
  3. | AllMatches
Sourceval eq_elimination_ref : orientation -> Sorts.family -> Names.GlobRef.t option
Sourceval rewriteLR : EConstr.constr -> unit Proofview.tactic
Sourceval rewriteRL : EConstr.constr -> unit Proofview.tactic
Sourceval 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
Sourceval 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
Sourcetype multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
Sourceval replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
Sourcetype inj_flags = {
  1. keep_proof_equalities : bool;
  2. injection_pattern_l2r_order : bool;
}
Sourceval discrConcl : unit Proofview.tactic
Sourceval discrHyp : Names.Id.t -> unit Proofview.tactic
Sourceval discrEverywhere : Tactics.evars_flag -> unit Proofview.tactic
Sourceexception NothingToInject
Sourceval 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
Sourceval injHyp : inj_flags option -> ?injection_in_context:bool -> Tactics.clear_flag -> Names.Id.t -> unit Proofview.tactic
Sourceval injConcl : inj_flags option -> ?injection_in_context:bool -> unit -> unit Proofview.tactic
Sourceval dEqThen : keep_proofs:bool option -> Tactics.evars_flag -> (int -> unit Proofview.tactic) -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
Sourceval cutRewriteInHyp : bool -> EConstr.types -> Names.Id.t -> unit Proofview.tactic
Sourceval cutRewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
Sourceval rewriteInHyp : bool -> EConstr.constr -> Names.Id.t -> unit Proofview.tactic
Sourceval rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
Sourceval set_keep_equality : Names.inductive -> bool -> unit
Sourcetype subst_tactic_flags = {
  1. only_leibniz : bool;
  2. rewrite_dependent_proof : bool;
}
Sourceval subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
Sourceval subst : Names.Id.t list -> unit Proofview.tactic
Sourceval subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
Sourceval replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
Sourceval set_eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind -> unit