Verified Commit f6389cbd authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Tentative changelog

parent 76cbd20a
Pipeline #48974 canceled with stage
in 3 minutes and 10 seconds
......@@ -33,6 +33,13 @@ Coq 8.11 is no longer supported in this version of Iris.
algorithm.
* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
`rFunctorContractive`, `urFunctorContractive`.
* Also set `Hint Mode` for the stdpp class `Equiv`.
This might require few spurious type annotations until
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
operand is a prefix of the other. The result is the longer list.
......
Markdown is supported
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