Skip to content
Snippets Groups Projects
Verified Commit c1d2615a authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

CHANGELOG: Unnest, and mention compatibility

parent afcea245
No related branches found
No related tags found
1 merge request!327countable.v: prove choose_proper
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 5 deletions
CHANGELOG.md
+ 5
− 5
View file @ c1d2615a
...@@ -172,11 +172,11 @@ API-breaking change is listed. ...@@ -172,11 +172,11 @@ API-breaking change is listed.
equal. equal.
- Add lemma `choose_proper` showing that `choose P` respects predicate - Add lemma `choose_proper` showing that `choose P` respects predicate
equivalence. (by Paolo G. Giarrusso, BedRock Systems) equivalence. (by Paolo G. Giarrusso, BedRock Systems)
- Well-founded definitions: Add induction principle `Acc_dep_ind`, a dependent - Extract module `well_founded` from `relations`, and re-export it for
version of `Acc_ind`. This lives in a new module `well_founded` together with compatibility. This contains `Acc_impl`, `wf_guard`, `wf_guard`,
some things that were previously found in `relations`: `Acc_impl`, `wf_guard`, `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
`wf_guard`, `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`. - Add induction principle `relations.Acc_dep_ind`, a dependent
(by Paolo G. Giarrusso, BedRock Systems) version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment