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.15.0.tar.gz | 0007215106 6.88 MB | |
| coq-refman-8.15.0.tar.xz | 0009211996 8.79 MB | |
| coq-rpmlintrc | 0000000340 340 Bytes | |
| coq-stdlib-8.15.0.tar.xz | 0002891876 2.76 MB | |
| coq.changes | 0000022256 21.7 KB | |
| coq.desktop | 0000000245 245 Bytes | |
| coq.spec | 0000008963 8.75 KB | |
| coq.xml | 0000000419 419 Bytes |
Revision 15 (latest revision is 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 946708
from
Aaron Puchert (aaronpuchert)
(revision 15)
- Update to version 8.15.0.
* The `apply with` tactic no longer renames arguments unless
the compatibility flag `Apply With Renaming` is set.
* Improvements to the `auto` tactic family, fixing `Hint Unfold`
behavior, and generalizing the use of discrimination nets.
* The `typeclasses eauto` tactic has a new `best_effort` option
allowing it to return partial solutions to a proof search
problem, depending on the mode declarations associated to each
constraint. This mode is used by typeclass resolution during
type inference to provide more precise error messages.
* Many commands and options were deprecated or removed after
deprecation and more consistently support locality attributes.
* The `Import` command is extended with `import_categories` to
select the components of a module to import or not, including
features such as hints, coercions, and notations.
* A visual Ltac debugger is now available in CoqIDE.
* For more details, see refman/changes.html in coq-doc.
Comments 0