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 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 =
| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
type inj_flags = {
keep_proof_equalities : bool;
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 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 set_keep_equality : Names.inductive -> bool -> unit
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