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:15.2:FactoryCandidates/coq && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| coq-8.11.1.tar.gz | 0006562343 6.26 MB | |
| coq-rpmlintrc | 0000000336 336 Bytes | |
| coq.changes | 0000012607 12.3 KB | |
| coq.desktop | 0000000245 245 Bytes | |
| coq.spec | 0000007179 7.01 KB | |
| coq.xml | 0000000419 419 Bytes |
Revision 4 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 792575
from
Aaron Puchert (aaronpuchert)
(revision 4)
- Update to version 8.11.1, with upstream support for OCaml 4.10.
* Allow more inductive types in Unset Positivity Checking mode.
* Fixed bugs in dealing with precedence of notations in custom
entries.
* In primitive floats, print a warning when parsing a decimal
value that is not exactly a binary64 floating-point number.
For instance, parsing 0.1 will print a warning whereas parsing
0.5 won't.
* Fixed an issue in CoqIDE about compiling file paths containing
spaces.
* Fixed an issue where Extraction Implicit on the constructor of
a record was leading to an anomaly.
- Remove now obsolete ocaml-410-build.patch.
Comments 0