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 |
|---|---|---|
| _constraints | 0000000219 219 Bytes | |
| coq-8.19.2.tar.gz | 0007678311 7.32 MB | |
| coq-refman-8.19.2.tar.xz | 0007665520 7.31 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.19.2.tar.xz | 0002176420 2.08 MB | |
| coq.changes | 0000032131 31.4 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 |
Latest Revision
Dominique Leuenberger (dimstar_suse)
accepted
request 1184115
from
Aaron Puchert (aaronpuchert)
(revision 28)
- Update to version 8.19.2.
* Fixed a regression from Coq 8.18 in the presence of a defined
field in a primitive `Record`.
* Fixed an issue where the printer was sometimes failing to use a
prefix or infix custom notation whose right-hand side refers to
a different custom entry.
* Fixed `abstract` failure in the presence of admitted goals in
the surrounding proof.
* Fixed issues when using Ltac2 in VsCoq due to incorrect state
handling of Ltac2 notations.
* Fixed `Include` on a module containing a record declared with
`Primitive Projections`.
* Fixed an issue in `Fixpoint` with no arguments.
* Position error/warning tooltips correctly when multibyte UTF-8
characters are present.
Comments 0