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:Leap:16.0:FactoryCandidates/coq && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| _constraints | 0000000165 165 Bytes | |
| coq-8.12.1.tar.gz | 0006855317 6.54 MB | |
| coq-rpmlintrc | 0000000336 336 Bytes | |
| coq.changes | 0000015475 15.1 KB | |
| coq.desktop | 0000000245 245 Bytes | |
| coq.spec | 0000007147 6.98 KB | |
| coq.xml | 0000000419 419 Bytes |
Revision 7 (latest revision is 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 849178
from
Aaron Puchert (aaronpuchert)
(revision 7)
- Update to version 8.12.1. This contains mostly bug fixes:
* Polymorphic side-effects inside monomorphic definitions were
incorrectly handled as not inlined. This allowed deriving an
inconsistency.
* Regression in error reporting after SSReflect's case tactic.
A generic error message "Could not fill dependent hole in
apply" was reported for any error following case or elim.
* Several bugs with Search.
* The details environment introduced in coqdoc in Coq 8.12 can
now be used as advertised in the reference manual.
* View menu "Display parentheses" introduced in CoqIDE in
Coq 8.12 now works correctly.
- Use memoryperjob constraint instead of %limit_build macro.
Comments 0