package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz

md5=8d852367b54f095d9fbabd000304d450

sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

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 coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssreflect_plugin/Ssreflect_plugin/Ssrfwd/index.html

Module Ssreflect_plugin.SsrfwdSource

Module `Ssreflect_plugin.Ssrfwd`Source