package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct