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:PowerPC/coq && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| _constraints | 0000000219 219 Bytes | |
| coq-8.16.1.tar.gz | 0007401345 7.06 MB | |
| coq-refman-8.16.1.tar.xz | 0009460272 9.02 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.16.1.tar.xz | 0002897632 2.76 MB | |
| coq.changes | 0000025621 25 KB | |
| coq.spec | 0000009223 9.01 KB | |
| coq.xml | 0000000419 419 Bytes | |
| fr.inria.coq.coqide.desktop | 0000000245 245 Bytes | |
| fr.inria.coq.coqide.metainfo.xml | 0000002905 2.84 KB |
Revision 19 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 1038367
from
Aaron Puchert (aaronpuchert)
(revision 19)
- Update to version 8.16.1.
* Fixed the conversion of `Prod` values in the native compiler.
* Added `SProp` check for opaque names in conversion.
* Pass the correct environment to compute η-expansion of
cofixpoints in VM and native compilation.
* Fixed an inconsistency with conversion of primitive arrays, and
associated incomplete strong normalization of primitive arrays
with `lazy`.
* `Print Assumptions` treats opaque definitions with missing
proofs (as found in .vos files, produced using -vos) as axioms
instead of ignoring them.
Comments 0