Overview
Request 946708 accepted
- 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.
- Created by aaronpuchert
- In state accepted
Request History
aaronpuchert created request
- 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.
factory-auto added opensuse-review-team as a reviewer
Please review sources
factory-auto accepted review
Check script succeeded
dimstar_suse added openSUSE:Factory:Staging:adi:7 as a reviewer
Being evaluated by staging project "openSUSE:Factory:Staging:adi:7"
dimstar_suse accepted review
Picked "openSUSE:Factory:Staging:adi:7"
licensedigger accepted review
The legal review is accepted preliminary. The package may require actions later on.
dimstar accepted review
dimstar_suse accepted review
Staging Project openSUSE:Factory:Staging:adi:7 got accepted.
dimstar_suse approved review
Staging Project openSUSE:Factory:Staging:adi:7 got accepted.
dimstar_suse accepted request
Staging Project openSUSE:Factory:Staging:adi:7 got accepted.