package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2+9.1.tar.gz
sha512=2147d2b41d18ea066ce8fb3e6fbe25be4293c4e1f6960e73843e4400b6b865ab6807aaaf098b4b5461a555cb2b7df7ea18db5dad56ce528e624f74e04b6eb64f
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:2025-11-14Published: 20 Nov 2025
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page