package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.3+9.1.tar.gz
sha512=9bf43af399df1e838e8c0c61b1d089899d5947da6704518db2734be93ce8682e6f42f066530e0a24a2d8113e0167e476896af3fa79b13047952617c6385735e1
Description
Collection of tactics that are used by the hammer for Coq to reconstruct proofs found by automated theorem provers. When the hammer has been successfully applied to a project, only this package needs to be installed; the hammer plugin is not required.
Tags
keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2026-07-06Published: 09 Jul 2026
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page