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.17.0.tar.gz

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

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