Skip to content
Snippets Groups Projects
Commit a76fec7a authored by Ralf Jung's avatar Ralf Jung
Browse files

tweak changelog

parent 5f5c02af
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 7 deletions
CHANGELOG.md
+ 3
− 7
View file @ a76fec7a
...@@ -33,13 +33,9 @@ Coq 8.11 is no longer supported in this version of Iris. ...@@ -33,13 +33,9 @@ Coq 8.11 is no longer supported in this version of Iris.
algorithm. algorithm.
* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`, * Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
`rFunctorContractive`, `urFunctorContractive`. `rFunctorContractive`, `urFunctorContractive`.
* Also set `Hint Mode` for the stdpp class `Equiv`. * Set `Hint Mode` for the stdpp class `Equiv`. This might require few spurious
This might require few spurious type annotations until type annotations until
https://github.com/coq/coq/issues/14441 is fixed. [Coq bug #14441](https://github.com/coq/coq/issues/14441) is fixed.
This `Hint Mode` is not in stdpp due to Coq bugs
https://github.com/coq/coq/issues/5735 and
https://github.com/coq/coq/issues/9058, only fixed in Coq >= 8.12, which stdpp
supports and Iris does not.
* Add `max_prefix_list` RA on lists whose composition is only defined when one * Add `max_prefix_list` RA on lists whose composition is only defined when one
operand is a prefix of the other. The result is the longer list. operand is a prefix of the other. The result is the longer list.
......
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