package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/ssreflect_plugin/Ssreflect_plugin/Ssrfwd/index.html
Module Ssreflect_plugin.SsrfwdSource
Source
val ssrsettac :
Names.Id.t ->
((Ssrast.ssrfwdfmt
* (Ssrmatching_plugin.Ssrmatching.cpattern * Ssrast.ast_closure_term option))
* Ssrast.ssrdocc) ->
unit Proofview.tacticSource
val ssrposetac :
(Names.Id.t * (Ssrast.ssrfwdfmt * Ssrast.ast_closure_term)) ->
unit Proofview.tacticSource
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.tacticSource
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.tacticSource
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.tacticSource
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