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.17.1.tar.gz | 0007506035 7.16 MB | |
| coq-refman-8.17.1.tar.xz | 0009623584 9.18 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.17.1.tar.xz | 0002930092 2.79 MB | |
| coq.changes | 0000027678 27 KB | |
| coq.spec | 0000008897 8.69 KB | |
| coq.xml | 0000000419 419 Bytes | |
| fr.inria.coq.coqide.desktop | 0000000235 235 Bytes | |
| fr.inria.coq.coqide.metainfo.xml | 0000003157 3.08 KB |
Revision 22 (latest revision is 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 1095883
from
Aaron Puchert (aaronpuchert)
(revision 22)
- Update to version 8.17.1.
* Fixed incorrect paths emitted by coqdep in some cases for META
files which prevented dune builds for plugins from working
correctly.
* Fixed shadowing of record fields in extraction to OCaml.
* Fixed an impossible-to-turn-off debug message "backtracking and
redoing byextend on ...".
* Fixed a major memory regression affecting MathComp 2.
- Classify desktop entry under Science instead of Education.
- Add screenshot URL to AppStream metadata.
Comments 0