Commit 458a3fa8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent c215b6cc
Pipeline #65866 passed with stage
in 4 minutes and 10 seconds
...@@ -6,7 +6,8 @@ API-breaking change is listed. ...@@ -6,7 +6,8 @@ API-breaking change is listed.
Coq 8.11 is no longer supported. Coq 8.11 is no longer supported.
- Make sure that `gset` and `mapset` do not bump the universe. - Make sure that `gset` and `mapset` do not bump the universe.
- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock Systems) - Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock
Systems)
- Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is - Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
now inferred automatically. To make this possible, getting the domain of a now inferred automatically. To make this possible, getting the domain of a
`gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
...@@ -14,6 +15,9 @@ Coq 8.11 is no longer supported. ...@@ -14,6 +15,9 @@ Coq 8.11 is no longer supported.
When combining `dom` with `≡`, this can run into an old issue (due to a Coq When combining `dom` with `≡`, this can run into an old issue (due to a Coq
issue, `Equiv` does not the desired `Hint Mode !`), which can make it issue, `Equiv` does not the desired `Hint Mode !`), which can make it
necessary to annotate the set type at the `≡` via `≡@{D}`. necessary to annotate the set type at the `≡` via `≡@{D}`.
- Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
`nclose_eq`. These unsealing lemmas are internal, so in principle you should
not rely on them.
## std++ 1.7.0 (2022-01-22) ## std++ 1.7.0 (2022-01-22)
......
Supports Markdown
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