The Coq Proof Assistant
Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.
- Developed at science
- Sources inherited from project openSUSE:Factory
-
1
derived packages
- Download package
-
Checkout Package
osc -A https://api.opensuse.org checkout openSUSE:Factory:zSystems/coq && cd $_
- Create Badge
Refresh
Refresh
Source Files
Filename | Size | Changed |
---|---|---|
coq-8.11.2.tar.gz | 0006564523 6.26 MB | |
coq-rpmlintrc | 0000000336 336 Bytes | |
coq.changes | 0000013227 12.9 KB | |
coq.desktop | 0000000245 245 Bytes | |
coq.spec | 0000007179 7.01 KB | |
coq.xml | 0000000419 419 Bytes |
Revision 5 (latest revision is 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 812064
from
Aaron Puchert (aaronpuchert)
(revision 5)
- Update to version 8.11.2. * Fixed a kernel issue where using Require inside a section caused an anomaly when closing the section. * Fixed normalization in conclusion of custom induction scheme. * Fixed a loss of location of some tactic errors. * Ignore -native-compiler option when built without native compute support. * Fixed a segfault issue with CoqIDE completion. * Highlighting style is now consistently applied to all three buffers of CoqIDE.
Comments 0