b65f8cd660
- Update to version 8.18.0.
* The default locality of `Hint` and `Instance` commands was
switched to `export`.
* The universe unification algorithm can now delay the commitment
to a sort (the algorithm used to pick `Type`). Thanks to this
feature many `Prop` and `SProp` annotations can be now omitted.
* Ltac2 supports array literals, maps and sets of primitive
datatypes such as names (of constants, inductive types, etc)
and fine-grained control over profiling.
* The warning system offers new categories, enabling finer
(de)activation of specific warnings. This should be
particularly useful to handle deprecations.
* Many new lemmas useful for teaching analysis with Coq are now
part of the standard library about real numbers.
* The `#[deprecated]` attribute can now be applied to definitions.
OBS-URL: https://build.opensuse.org/request/show/1111685
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=23
|
||
|---|---|---|
| _constraints | ||
| .gitattributes | ||
| .gitignore | ||
| coq-8.18.0.tar.gz | ||
| coq-refman-8.18.0.tar.xz | ||
| coq-rpmlintrc | ||
| coq-stdlib-8.18.0.tar.xz | ||
| coq.changes | ||
| coq.spec | ||
| coq.xml | ||
| fr.inria.coq.coqide.desktop | ||
| fr.inria.coq.coqide.metainfo.xml | ||