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.15.2.tar.gz | 0007222794 6.89 MB | |
| coq-refman-8.15.2.tar.xz | 0009221052 8.79 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.15.2.tar.xz | 0002892408 2.76 MB | |
| coq.changes | 0000023606 23.1 KB | |
| coq.spec | 0000009232 9.02 KB | |
| coq.xml | 0000000419 419 Bytes | |
| fr.inria.coq.coqide.desktop | 0000000245 245 Bytes | |
| fr.inria.coq.coqide.metainfo.xml | 0000002805 2.74 KB |
Revision 17 (latest revision is 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 980409
from
Aaron Puchert (aaronpuchert)
(revision 17)
- Update to version 8.15.2.
* Tactics `intuition` and `dintuition` use
`Tauto.intuition_solver` (defined as `auto with *`) instead of
hardcoding `auto with *`. This makes it possible to change the
default solver with `Ltac Tauto.intuition_solver ::= ...`.
* Fixed an uncaught exception `UnableToUnify` with
bidirectionality hints.
* Fixed multiple CoqIDE bugs.
* Fixed an incorrect implementation of `SFClassify`, allowing for
a proof of `False` since 8.11.0, due to Axioms present in
`Float.Axioms`.
- Rename coq.desktop to fr.inria.coq.coqide.desktop as the
documentation suggests, add an accompanying metainfo file.
- Declare documentation as noarch.
Comments 0