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.19.1.tar.gz | 0007675945 7.32 MB | |
| coq-refman-8.19.1.tar.xz | 0007616556 7.26 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.19.1.tar.xz | 0002148396 2.05 MB | |
| coq.changes | 0000031258 30.5 KB | |
| coq.spec | 0000009498 9.28 KB | |
| coq.xml | 0000000419 419 Bytes | |
| fr.inria.coq.coqide.desktop | 0000000235 235 Bytes | |
| fr.inria.coq.coqide.metainfo.xml | 0000003357 3.28 KB |
Revision 27 (latest revision is 29)
Ana Guerrero (anag+factory)
accepted
request 1156169
from
Aaron Puchert (aaronpuchert)
(revision 27)
- Update to version 8.19.1.
* Fixed incorrect abstraction of sort variables for opaque
constants leading to an inconsistency.
* Fixed memory corruption with `vm_compute` (rare but more
likely with OCaml 5.1).
* "Found no matching notation to enable or disable" is now a
warning instead of an error.
* Fixed undeclared universe with multiple uses of `abstract`.
* Fixed incorrect printing of constructor values with multiple
arguments, and over-parenthesizing of constructor printing.
* Fixed incorrect declared type for Ltac2.FMap.fold.
Comments 0