package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/ssreflect_plugin/Ssreflect_plugin/Ssrtacticals/index.html
Module Ssreflect_plugin.SsrtacticalsSource
Source
val tclSEQAT :
Ltac_plugin.Tacinterp.interp_sign ->
Ltac_plugin.Tacinterp.Value.t ->
Ssrast.ssrdir ->
(int Locus.or_var
* (('a * Ltac_plugin.Tacinterp.Value.t option list)
* Ltac_plugin.Tacinterp.Value.t option)) ->
unit Proofview.tacticSource
val tclCLAUSES :
unit Proofview.tactic ->
((Ssrast.ssrhyps
* ((Ssrast.ssrhyp_or_id * string)
* Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
list
* Ssrast.ssrclseq) ->
unit Proofview.tacticSource
val hinttac :
Ltac_plugin.Tacinterp.interp_sign ->
bool ->
(bool * Ltac_plugin.Tacinterp.Value.t option list) ->
unit Proofview.tacticSource
val ssrdotac :
Ltac_plugin.Tacinterp.interp_sign ->
(((int Locus.or_var * Ssrast.ssrmmod)
* (bool * Ltac_plugin.Tacinterp.Value.t option list))
* ((Ssrast.ssrhyps
* ((Ssrast.ssrhyp_or_id * string)
* Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
list
* Ssrast.ssrclseq)) ->
unit Proofview.tactic