The Coq Proof Assistant

Edit Package coq

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.

Refresh
Refresh
Source Files
Filename Size Changed
_constraints 0000000219 219 Bytes
coq-8.19.1.tar.gz 0007675945 7.32 MB
coq-refman-8.19.1.tar.xz 0007616556 7.26 MB
coq-rpmlintrc 0000000340 340 Bytes
coq-stdlib-8.19.1.tar.xz 0002148396 2.05 MB
coq.changes 0000031258 30.5 KB
coq.spec 0000009498 9.28 KB
coq.xml 0000000419 419 Bytes
fr.inria.coq.coqide.desktop 0000000235 235 Bytes
fr.inria.coq.coqide.metainfo.xml 0000003357 3.28 KB
Latest Revision
Ana Guerrero's avatar Ana Guerrero (anag+factory) accepted request 1156169 from Aaron Puchert's avatar Aaron Puchert (aaronpuchert) (revision 27)
- Update to version 8.19.1.
  * Fixed incorrect abstraction of sort variables for opaque
    constants leading to an inconsistency.
  * Fixed memory corruption with `vm_compute` (rare but more
    likely with OCaml 5.1).
  * "Found no matching notation to enable or disable" is now a
    warning instead of an error.
  * Fixed undeclared universe with multiple uses of `abstract`.
  * Fixed incorrect printing of constructor values with multiple
    arguments, and over-parenthesizing of constructor printing.
  * Fixed incorrect declared type for Ltac2.FMap.fold.
Comments 0
openSUSE Build Service is sponsored by