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 | 0000000219 219 Bytes | |
| coq-8.15.1.tar.gz | 0007221470 6.89 MB | |
| coq-refman-8.15.1.tar.xz | 0009213172 8.79 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.15.1.tar.xz | 0002892604 2.76 MB | |
| coq.changes | 0000022774 22.2 KB | |
| coq.desktop | 0000000245 245 Bytes | |
| coq.spec | 0000008963 8.75 KB | |
| coq.xml | 0000000419 419 Bytes |
Revision 16 (latest revision is 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 964734
from
Aaron Puchert (aaronpuchert)
(revision 16)
- Update to version 8.15.1.
* Fixes an inconsistency when using module subtyping with
inductive types.
* Speeds up CoqIDE on large files.
* Fixes a bug where `coqc -vok` was not creating a .vok file.
* Fixes a regression in `cbn`.
* Improves usability of schemes with `elim foo using scheme with
(P0 := ...)` (the `P0` name was not accessible in 8.15.0).
Comments 0