Equality (p.coq.8.16.1.doc.coq-core.tactics.Equality)

Sourcetype dep_proof_flag = bool

Sourcetype freeze_evars_flag = bool

Sourcetype orientation = bool

Sourcetype conditions =

| Naive
| FirstSolved
| 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

Source

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

Source

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

Sourcetype multi =

| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus

Source

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

Source

val replace_in_clause_maybe_by : 
  EConstr.constr ->
  EConstr.constr ->
  Locus.clause ->
  unit Proofview.tactic option ->
  unit Proofview.tactic

Sourceval replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Source

val replace_by : 
  EConstr.constr ->
  EConstr.constr ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourcetype inj_flags = {

keep_proof_equalities : bool;
injection_pattern_l2r_order : bool;

}

Source

val discr : 
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

Sourceval discrConcl : unit Proofview.tactic

Sourceval discrHyp : Names.Id.t -> unit Proofview.tactic

Sourceval discrEverywhere : Tactics.evars_flag -> unit Proofview.tactic

Source

val discr_tac : 
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Sourceexception NothingToInject

Source

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

Source

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

Source

val injHyp : 
  inj_flags option ->
  ?injection_in_context:bool ->
  Tactics.clear_flag ->
  Names.Id.t ->
  unit Proofview.tactic

Source

val injConcl : 
  inj_flags option ->
  ?injection_in_context:bool ->
  unit ->
  unit Proofview.tactic

Source

val simpleInjClause : 
  inj_flags option ->
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Source

val dEq : 
  keep_proofs:bool option ->
  Tactics.evars_flag ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Source

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

Source

val make_iterated_tuple : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (EConstr.constr * EConstr.types) ->
  Evd.evar_map * (EConstr.constr * EConstr.constr * EConstr.constr)

Source

val cutRewriteInHyp : 
  bool ->
  EConstr.types ->
  Names.Id.t ->
  unit Proofview.tactic

Sourceval cutRewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic

Source

val rewriteInHyp : 
  bool ->
  EConstr.constr ->
  Names.Id.t ->
  unit Proofview.tactic

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

Source

val discriminable : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

val injectable : 
  Environ.env ->
  Evd.evar_map ->
  keep_proofs:bool option ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Sourceval set_keep_equality : Names.inductive -> bool -> unit

Sourcetype subst_tactic_flags = {

only_leibniz : bool;
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

Source

val 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

Source

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