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.16.0.tar.gz | 0007397421 7.05 MB | |
coq-refman-8.16.0.tar.xz | 0009458828 9.02 MB | |
coq-rpmlintrc | 0000000340 340 Bytes | |
coq-stdlib-8.16.0.tar.xz | 0002897452 2.76 MB | |
coq.changes | 0000024909 24.3 KB | |
coq.spec | 0000009223 9.01 KB | |
coq.xml | 0000000419 419 Bytes | |
fr.inria.coq.coqide.desktop | 0000000245 245 Bytes | |
fr.inria.coq.coqide.metainfo.xml | 0000002855 2.79 KB |
Revision 18 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 1002206
from
Aaron Puchert (aaronpuchert)
(revision 18)
- Update to version 8.16.0. * The guard checker (see `Guarded`) now ensures strong normalization under any reduction strategy. * Irrelevant terms (in the `SProp` sort) are now squashed to a dummy value during conversion, fixing a subject reduction issue and making proof conversion faster. * Introduction of reversible coercions, which allow coercions relying on meta-level resolution such as type-classes or canonical structures. Also allow coercions that do not fullfill the uniform inheritance condition. * Generalized rewriting support for rewriting with `Type`-valued relations and in `Type` contexts, using the `Classes.CMorphisms` library. * Added the boolean equality scheme command for decidable inductive types. * Added a `Print Notation` command. * Incompatibilities in name generation for Program obligations, `eauto` treatment of tactic failure levels, use of `ident` in notations, parsing of module expressions. * Standard library reorganization and deprecations. * Improve the treatment of standard library numbers by `Extraction`. - Coq requires ocamlfind at runtime now.
Comments 0