Module Equality

type dep_proof_flag = bool
type freeze_evars_flag = bool
type orientation = bool
type conditions =
| Naive
| FirstSolved
| AllMatches
val eq_elimination_ref : orientation -> Sorts.family -> Names.GlobRef.t option
val general_rewrite_bindings : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> EConstr.constr Tactypes.with_bindings -> Tactics.evars_flag -> unit Proofview.tactic
val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
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
val general_rewrite_ebindings_clause : Names.Id.t option -> orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> EConstr.constr Tactypes.with_bindings -> Tactics.evars_flag -> unit Proofview.tactic
val general_rewrite_bindings_in : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> Names.Id.t -> EConstr.constr Tactypes.with_bindings -> Tactics.evars_flag -> unit Proofview.tactic
val general_rewrite_in : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> Names.Id.t -> EConstr.constr -> Tactics.evars_flag -> unit Proofview.tactic
val general_rewrite_clause : orientation -> Tactics.evars_flag -> ?⁠tac:(unit Proofview.tactic * conditions) -> EConstr.constr Tactypes.with_bindings -> Locus.clause -> unit Proofview.tactic
type multi =
| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus
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
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val replace_by : EConstr.constr -> EConstr.constr -> unit Proofview.tactic -> unit Proofview.tactic
type inj_flags = {
keep_proof_equalities : bool;
injection_in_context : bool;
injection_pattern_l2r_order : bool;
}
val discr : Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val discrConcl : unit Proofview.tactic
val discrHyp : Names.Id.t -> unit Proofview.tactic
val discrEverywhere : Tactics.evars_flag -> unit Proofview.tactic
val discr_tac : Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val inj : inj_flags option -> Tactypes.intro_patterns option -> Tactics.evars_flag -> Tactics.clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val injClause : inj_flags option -> Tactypes.intro_patterns option -> Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val injHyp : inj_flags option -> Tactics.clear_flag -> Names.Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> unit Proofview.tactic
val simpleInjClause : inj_flags option -> Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val dEq : keep_proofs:bool option -> Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val dEqThen : keep_proofs:bool option -> Tactics.evars_flag -> (Tactics.clear_flag -> EConstr.constr -> int -> unit Proofview.tactic) -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple : Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.constr * EConstr.types) -> Evd.evar_map * (EConstr.constr * EConstr.constr * EConstr.constr)
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 = {
only_leibniz : bool;
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
val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> EConstr.constr -> EConstr.constr -> EConstr.constr