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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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