Overview
Request 1002206 accepted
- Update to version 8.16.0.
* The guard checker (see `Guarded`) now ensures strong
normalization under any reduction strategy.
* Irrelevant terms (in the `SProp` sort) are now squashed to a
dummy value during conversion, fixing a subject reduction
issue and making proof conversion faster.
* Introduction of reversible coercions, which allow coercions
relying on meta-level resolution such as type-classes or
canonical structures. Also allow coercions that do not fullfill
the uniform inheritance condition.
* Generalized rewriting support for rewriting with `Type`-valued
relations and in `Type` contexts, using the
`Classes.CMorphisms` library.
* Added the boolean equality scheme command for decidable
inductive types.
* Added a `Print Notation` command.
* Incompatibilities in name generation for Program obligations,
`eauto` treatment of tactic failure levels, use of `ident` in
notations, parsing of module expressions.
* Standard library reorganization and deprecations.
* Improve the treatment of standard library numbers by
`Extraction`.
- Coq requires ocamlfind at runtime now.
- Created by aaronpuchert
- In state accepted
Request History
aaronpuchert created request
- Update to version 8.16.0.
* The guard checker (see `Guarded`) now ensures strong
normalization under any reduction strategy.
* Irrelevant terms (in the `SProp` sort) are now squashed to a
dummy value during conversion, fixing a subject reduction
issue and making proof conversion faster.
* Introduction of reversible coercions, which allow coercions
relying on meta-level resolution such as type-classes or
canonical structures. Also allow coercions that do not fullfill
the uniform inheritance condition.
* Generalized rewriting support for rewriting with `Type`-valued
relations and in `Type` contexts, using the
`Classes.CMorphisms` library.
* Added the boolean equality scheme command for decidable
inductive types.
* Added a `Print Notation` command.
* Incompatibilities in name generation for Program obligations,
`eauto` treatment of tactic failure levels, use of `ident` in
notations, parsing of module expressions.
* Standard library reorganization and deprecations.
* Improve the treatment of standard library numbers by
`Extraction`.
- Coq requires ocamlfind at runtime now.
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:10 as a reviewer
Being evaluated by staging project "openSUSE:Factory:Staging:adi:10"
staging-bot accepted review
Picked "openSUSE:Factory:Staging:adi:10"
dimstar accepted review
dimstar_suse accepted review
Staging Project openSUSE:Factory:Staging:adi:10 got accepted.
dimstar_suse approved review
Staging Project openSUSE:Factory:Staging:adi:10 got accepted.
dimstar_suse accepted request
Staging Project openSUSE:Factory:Staging:adi:10 got accepted.