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/ssreflect_plugin/Ssreflect_plugin/Ssrfwd/index.html

Module `Ssreflect_plugin.Ssrfwd`Source

Source

val ssrsettac : 
  Names.Id.t ->
  ((Ssrast.ssrfwdfmt
    * (Ssrmatching_plugin.Ssrmatching.cpattern * Ssrast.ast_closure_term option))
   * Ssrast.ssrdocc) ->
  unit Proofview.tactic

Source

val ssrposetac : 
  (Names.Id.t * (Ssrast.ssrfwdfmt * Ssrast.ast_closure_term)) ->
  unit Proofview.tactic

Source

val havetac : 
  Ssrast.ist ->
  (bool
   * ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats)
       * Ssrast.ssripats)
      * (((Ssrast.ssrfwdkind * 'a) * Ssrast.ast_closure_term)
         * (bool * Ltac_plugin.Tacinterp.Value.t option list)))) ->
  bool ->
  bool ->
  unit Proofview.tactic

Sourcetype cut_kind =

| Have
| HaveTransp
| Suff

Sourceval basecuttac : cut_kind -> EConstr.t -> unit Proofview.tactic

Sourceval basesufftac : EConstr.t -> unit Proofview.tactic

Source

val wlogtac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  (((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b) ->
  ((Ssrast.ssrhyps
    * ((Ssrast.ssrhyp_or_id * string)
       * Ssrmatching_plugin.Ssrmatching.cpattern option)
        option)
     list
   * ('c * Ssrast.ast_closure_term)) ->
  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
  bool ->
  [< `Gen of Names.Id.t option option | `NoGen NoGen ] ->
  unit Proofview.tactic

Source

val sufftac : 
  Ssrast.ist ->
  ((((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list)
    * Ssrast.ssripat list)
   * (('a * Ssrast.ast_closure_term)
      * (bool * Ltac_plugin.Tacinterp.Value.t option list))) ->
  unit Proofview.tactic

Source

val undertac : 
  ?pad_intro:bool ->
  Ltac_plugin.Tacinterp.interp_sign ->
  Ssrast.ssripats option ->
  Ssrequality.ssrrwarg ->
  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
  unit Proofview.tactic

Sourceval overtac : unit Proofview.tactic

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssreflect_plugin/Ssreflect_plugin/Ssrfwd/index.html

Module Ssreflect_plugin.SsrfwdSource

Module `Ssreflect_plugin.Ssrfwd`Source