package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.3+9.2.tar.gz
sha512=6547d6824795a7f3d0281c0931be2c63571443a28df7467dfe7caa0380845653a3f1a61c71550ff3bd64c18b2694336c2e04a412e65ea9bddcdb3d2b5aa940d9
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-07Published: 09 Jul 2026
Dependencies (3)
-
rocq-stdlib
>= "9.1" & < "9.3~" -
rocq-core
>= "9.2" & < "9.3~" -
ocaml
>= "4.09"
Dev Dependencies
None
Used by (1)
-
coq-hammer
>= "1.3.3+9.2"
Conflicts (1)
-
coq-hammer
!= version
On This Page