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.17.0.tar.gz | 0007504612 7.16 MB | |
coq-refman-8.17.0.tar.xz | 0009630296 9.18 MB | |
coq-rpmlintrc | 0000000340 340 Bytes | |
coq-stdlib-8.17.0.tar.xz | 0002929684 2.79 MB | |
coq.changes | 0000027039 26.4 KB | |
coq.spec | 0000008897 8.69 KB | |
coq.xml | 0000000419 419 Bytes | |
fr.inria.coq.coqide.desktop | 0000000245 245 Bytes | |
fr.inria.coq.coqide.metainfo.xml | 0000002955 2.89 KB |
Revision 21 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 1075082
from
Aaron Puchert (aaronpuchert)
(revision 21)
- Update to version 8.17.0. * Fixed a logical inconsistency due to `vm_compute` in presence of side-effects in the enviroment (e.g. using Back or Fail). * It is now possible to dynamically enable or disable notations. * Support multiple scopes in `Arguments` and `Bind Scope`. * The tactics chapter of the manual has many improvements in presentation and wording. The documented grammar is semi- automatically checked for consistency with the implementation. * Fixes to the `auto` and `eauto` tactics, to respect hint priorities and the documented use of simple apply. This is a potentially breaking change. * New Ltac2 APIs, deep pattern-matching with `as` clauses and handling of literals, support for record types and preterms. * Move from :> to :: syntax for declaring typeclass fields as instances, fixing a confusion with declaration of coercions. * Standard library improvements.
Comments 0