Equality (rocq-runtime.Equality)

type dep_proof_flag = bool

type freeze_evars_flag = bool

type orientation = bool

type conditions =

| Naive
| FirstSolved
| AllMatches

val lookup_eq_eliminator_with_error : 
  ?het_eq:bool ->
  Environ.env ->
  Evd.evar_map ->
  Evd.econstr ->
  dep:bool ->
  inccl:bool ->
  l2r:orientation ->
  c_sort:EConstr.ESorts.t ->
  e_sort:EConstr.ESorts.t ->
  p_sort:EConstr.ESorts.t ->
  (Evd.evar_map * Evd.econstr) * Tactics.equality_position_on_elim

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 : 
  bool option ->
  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 rewriteInHyp : 
  bool ->
  EConstr.constr ->
  Names.Id.t ->
  unit Proofview.tactic

val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic

val set_keep_equality : Libobject.locality -> 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