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/Ssrequality/index.html
Module Ssreflect_plugin.SsrequalitySource
Source
type ssrrwarg =
(Ssrast.ssrdir * Ssrast.ssrmult)
* ((Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.rpattern option)
* ssrrule)Source
val newssrcongrtac :
(int * Ssrast.ssrterm) ->
Ltac_plugin.Tacinterp.interp_sign ->
unit Proofview.tacticSource
val mk_rwarg :
(Ssrast.ssrdir * (int * Ssrast.ssrmmod)) ->
((Ssrast.ssrclear option * Ssrast.ssrocc)
* Ssrmatching_plugin.Ssrmatching.rpattern option) ->
(ssrwkind * Ssrast.ssrterm) ->
ssrrwargSource
val norwocc :
(Ssrast.ssrclear option * Ssrast.ssrocc)
* Ssrmatching_plugin.Ssrmatching.rpattern optionSource
val ssrinstancesofrule :
Ltac_plugin.Tacinterp.interp_sign ->
Ssrast.ssrdir ->
Ssrast.ssrterm ->
unit Proofview.tacticSource
val ssrrewritetac :
?under:bool ->
?map_redex:
(Environ.env ->
Evd.evar_map ->
before:EConstr.t ->
after:EConstr.t ->
Evd.evar_map * EConstr.t) ->
Ltac_plugin.Tacinterp.interp_sign ->
ssrrwarg list ->
unit Proofview.tacticSource
val unlocktac :
Ltac_plugin.Tacinterp.interp_sign ->
(Ssrmatching_plugin.Ssrmatching.occ * Ssrast.ssrterm) list ->
unit Proofview.tactic