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:Backports:SLE-15-SP4:FactoryCandidates/coq && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| _constraints | 0000000219 219 Bytes | |
| coq-8.14.1.tar.gz | 0007066759 6.74 MB | |
| coq-refman-8.14.1.tar.xz | 0009060468 8.64 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.14.1.tar.xz | 0002882676 2.75 MB | |
| coq.changes | 0000021087 20.6 KB | |
| coq.desktop | 0000000245 245 Bytes | |
| coq.spec | 0000008890 8.68 KB | |
| coq.xml | 0000000419 419 Bytes |
Revision 14 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 940115
from
Aaron Puchert (aaronpuchert)
(revision 14)
- Update to version 8.14.1.
* Fixed the implementation of persistent arrays used by the VM
and native compute so that it uses a uniform representation.
Previously, storing primitive floats inside primitive arrays
could cause memory corruption.
* Fixed missing registration of universe constraints in Module
Type elaboration.
* Made `abstract` more robust with respect to Ltac `constr`
bindings containing existential variables.
* Correct support of trailing `let` by tactic `specialize`.
* Fixed an anomaly with `Extraction Conservative Types` when
extracting pattern-matching on singleton types.
* Regular error instead of an anomaly when calling `Separate
Extraction` in a module.
Comments 0