package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.16.0.tar.gz

sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssreflect_plugin/Ssreflect_plugin/Ssrfwd/index.html

Module Ssreflect_plugin.SsrfwdSource

Module `Ssreflect_plugin.Ssrfwd`Source