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:Rebuild/coq && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| _constraints | 0000000219 219 Bytes | |
| coq-8.18.0.tar.gz | 0007612742 7.26 MB | |
| coq-refman-8.18.0.tar.xz | 0007492340 7.15 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.18.0.tar.xz | 0002205680 2.1 MB | |
| coq.changes | 0000028666 28 KB | |
| coq.spec | 0000008924 8.71 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 23 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 1111685
from
Aaron Puchert (aaronpuchert)
(revision 23)
- Update to version 8.18.0.
* The default locality of `Hint` and `Instance` commands was
switched to `export`.
* The universe unification algorithm can now delay the commitment
to a sort (the algorithm used to pick `Type`). Thanks to this
feature many `Prop` and `SProp` annotations can be now omitted.
* Ltac2 supports array literals, maps and sets of primitive
datatypes such as names (of constants, inductive types, etc)
and fine-grained control over profiling.
* The warning system offers new categories, enabling finer
(de)activation of specific warnings. This should be
particularly useful to handle deprecations.
* Many new lemmas useful for teaching analysis with Coq are now
part of the standard library about real numbers.
* The `#[deprecated]` attribute can now be applied to definitions.
Comments 0