package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.tactics/Equality/index.html

Module `Equality`Source

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 : 
  bool option ->
  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 ->
  (int -> unit Proofview.tactic) ->
  EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option ->
  unit Proofview.tactic

Source

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

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

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

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.tactics/Equality/index.html

Module EqualitySource

Module `Equality`Source