package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz

md5=0cfaa70f569be9494d24c829e6555d46

sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.tactics/Equality/index.html

Module `Equality`Source

Sourcetype dep_proof_flag = bool

Sourcetype freeze_evars_flag = bool

Sourcetype orientation = bool

Sourcetype conditions =

| Naive
| FirstSolved
| 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

Source

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

Source

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

Sourcetype multi =

| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus

Source

val general_multi_rewrite : 
  Tactics.evars_flag ->
  (bool
   * multi
   * Tactics.clear_flag
   * Tactypes.delayed_open_constr_with_bindings)
    list ->
  Locus.clause ->
  (unit Proofview.tactic * conditions) option ->
  unit Proofview.tactic

Source

val replace_in_clause_maybe_by : 
  bool option ->
  EConstr.constr ->
  EConstr.constr ->
  Locus.clause ->
  unit Proofview.tactic option ->
  unit Proofview.tactic

Sourceval replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Source

val replace_by : 
  EConstr.constr ->
  EConstr.constr ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourcetype inj_flags = {

keep_proof_equalities : bool;
injection_pattern_l2r_order : bool;

}

Source

val discr : 
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

Sourceval discrConcl : unit Proofview.tactic

Sourceval discrHyp : Names.Id.t -> unit Proofview.tactic

Sourceval discrEverywhere : Tactics.evars_flag -> unit Proofview.tactic

Source

val discr_tac : 
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Sourceexception NothingToInject

Source

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

Source

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

Source

val injHyp : 
  inj_flags option ->
  ?injection_in_context:bool ->
  Tactics.clear_flag ->
  Names.Id.t ->
  unit Proofview.tactic

Source

val injConcl : 
  inj_flags option ->
  ?injection_in_context:bool ->
  unit ->
  unit Proofview.tactic

Source

val simpleInjClause : 
  inj_flags option ->
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Source

val dEq : 
  keep_proofs:bool option ->
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Source

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

Source

val 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 = {

only_leibniz : bool;
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

Source

val 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

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.tactics/Equality/index.html

Module EqualitySource

Module `Equality`Source