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:PowerPC/coq && cd $_
- Create Badge
Refresh
Refresh
Source Files
Filename | Size | Changed |
---|---|---|
_constraints | 0000000219 219 Bytes | |
coq-8.19.0.tar.gz | 0007674352 7.32 MB | |
coq-refman-8.19.0.tar.xz | 0007608812 7.26 MB | |
coq-rpmlintrc | 0000000340 340 Bytes | |
coq-stdlib-8.19.0.tar.xz | 0002148484 2.05 MB | |
coq.changes | 0000030548 29.8 KB | |
coq.spec | 0000009522 9.3 KB | |
coq.xml | 0000000419 419 Bytes | |
fr.inria.coq.coqide.desktop | 0000000235 235 Bytes | |
fr.inria.coq.coqide.metainfo.xml | 0000003157 3.08 KB |
Revision 26 (latest revision is 27)
Ana Guerrero (anag+factory)
accepted
request 1142140
from
Aaron Puchert (aaronpuchert)
(revision 26)
- Update to version 8.19.0. The most impactful changes: * Sort polymorphism makes it possible to share common constructs over `Type`, `Prop` and `SProp`. * The notation `term%_scope` to set a scope only temporarily (in addition to `term%scope` for opening a scope applying to all subterms). * `lazy`, `simpl`, `cbn` and `cbv` and the associated `Eval` and `eval` reductions learned to do head reduction when given flag `head`. * New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of Ltac2 term patterns. * New performance evaluation facilities: `Instructions` to count CPU instructions used by a command and Profiling system to produce trace files. * New command `Attributes` to assign attributes such as `deprecated` to a library file. - Notable breaking changes: * `replace` with `by tac` does not automatically attempt to solve the generated equality subgoal using the hypotheses. Use `by first [assumption | symmetry;assumption | tac]` if you need the previous behaviour. * Removed old deprecated files from the standard library. - Use %fdupes in the documentation package.
Comments 0