Overview
Request 1111685 accepted
- 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.
- Created by aaronpuchert
- In state accepted
Request History
aaronpuchert created request
- 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.
factory-auto added opensuse-review-team as a reviewer
Please review sources
factory-auto accepted review
Check script succeeded
licensedigger accepted review
ok
staging-bot added openSUSE:Factory:Staging:adi:11 as a reviewer
Being evaluated by staging project "openSUSE:Factory:Staging:adi:11"
staging-bot accepted review
Picked "openSUSE:Factory:Staging:adi:11"
bigironman accepted review
Accepted review for by_group opensuse-review-team request 1111685 from user staging-bot
dimstar_suse accepted review
Staging Project openSUSE:Factory:Staging:adi:11 got accepted.
dimstar_suse approved review
Staging Project openSUSE:Factory:Staging:adi:11 got accepted.
dimstar_suse accepted request
Staging Project openSUSE:Factory:Staging:adi:11 got accepted.