Equality (coq-core.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 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_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

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 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 ->
  ( 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 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

val build_selector : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  EConstr.constr ->
  EConstr.types ->
  EConstr.constr ->
  EConstr.constr ->
  EConstr.constr