package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4
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