package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/ssreflect_plugin/Ssreflect_plugin/Ssrelim/index.html

Module Ssreflect_plugin.SsrelimSource

Sourceval ssrelim : ?is_case:bool -> ((Ssrast.ssrhyps option * Ssrast.ssrocc) * Ssrmatching_plugin.Ssrmatching.cpattern) list -> elim_what -> ?elim:EConstr.constr -> Ssrast.ssripat option -> (?seed:Names.Name.t list array -> elim_what -> Ssrast.ssripat option -> unit Proofview.tactic -> bool -> Ssrast.ssrhyp list -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval casetac : EConstr.constr -> (?seed:Names.Name.t list array -> unit Proofview.tactic -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval is_injection_case : Environ.env -> Evd.evar_map -> EConstr.t -> bool
Sourceval perform_injection : EConstr.constr -> unit Proofview.tactic
Sourceval ssrscase_or_inj_tac : EConstr.constr -> unit Proofview.tactic